Step |
Hyp |
Ref |
Expression |
1 |
|
xpss |
⊢ ( 𝑉 × 𝑊 ) ⊆ ( V × V ) |
2 |
1
|
sseli |
⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 ∈ ( V × V ) ) |
3 |
|
eqid |
⊢ ( 2nd ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) |
4 |
|
eqopi |
⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) ) ) → 𝐴 = 〈 𝐵 , ( 2nd ‘ 𝐴 ) 〉 ) |
5 |
3 4
|
mpanr2 |
⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( 1st ‘ 𝐴 ) = 𝐵 ) → 𝐴 = 〈 𝐵 , ( 2nd ‘ 𝐴 ) 〉 ) |
6 |
|
fvex |
⊢ ( 2nd ‘ 𝐴 ) ∈ V |
7 |
|
opeq2 |
⊢ ( 𝑥 = ( 2nd ‘ 𝐴 ) → 〈 𝐵 , 𝑥 〉 = 〈 𝐵 , ( 2nd ‘ 𝐴 ) 〉 ) |
8 |
7
|
eqeq2d |
⊢ ( 𝑥 = ( 2nd ‘ 𝐴 ) → ( 𝐴 = 〈 𝐵 , 𝑥 〉 ↔ 𝐴 = 〈 𝐵 , ( 2nd ‘ 𝐴 ) 〉 ) ) |
9 |
6 8
|
spcev |
⊢ ( 𝐴 = 〈 𝐵 , ( 2nd ‘ 𝐴 ) 〉 → ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 ) |
10 |
5 9
|
syl |
⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( 1st ‘ 𝐴 ) = 𝐵 ) → ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 ) |
11 |
10
|
ex |
⊢ ( 𝐴 ∈ ( V × V ) → ( ( 1st ‘ 𝐴 ) = 𝐵 → ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 ) ) |
12 |
|
eqop |
⊢ ( 𝐴 ∈ ( V × V ) → ( 𝐴 = 〈 𝐵 , 𝑥 〉 ↔ ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = 𝑥 ) ) ) |
13 |
|
simpl |
⊢ ( ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = 𝑥 ) → ( 1st ‘ 𝐴 ) = 𝐵 ) |
14 |
12 13
|
syl6bi |
⊢ ( 𝐴 ∈ ( V × V ) → ( 𝐴 = 〈 𝐵 , 𝑥 〉 → ( 1st ‘ 𝐴 ) = 𝐵 ) ) |
15 |
14
|
exlimdv |
⊢ ( 𝐴 ∈ ( V × V ) → ( ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 → ( 1st ‘ 𝐴 ) = 𝐵 ) ) |
16 |
11 15
|
impbid |
⊢ ( 𝐴 ∈ ( V × V ) → ( ( 1st ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 ) ) |
17 |
2 16
|
syl |
⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( ( 1st ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = 〈 𝐵 , 𝑥 〉 ) ) |