Metamath Proof Explorer


Theorem op1steq

Description: Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013) (Revised by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion op1steq ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( ( 1st𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )

Proof

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𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )