This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opth1

Description: Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses opth1.1 ⊢ 𝐴 ∈ V
opth1.2 ⊢ 𝐵 ∈ V
Assertion opth1 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )

Proof

Step Hyp Ref Expression
1 opth1.1 ⊢ 𝐴 ∈ V
2 opth1.2 ⊢ 𝐵 ∈ V
3 1 2 opi1 ⊢ { 𝐴 } ∈ ⟨ 𝐴 , 𝐵 ⟩
4 id ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
5 3 4 eleqtrid ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ )
6 1 sneqr ⊢ ( { 𝐴 } = { 𝐶 } → 𝐴 = 𝐶 )
7 6 a1i ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( { 𝐴 } = { 𝐶 } → 𝐴 = 𝐶 ) )
8 oprcl ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
9 8 simpld ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 ∈ V )
10 prid1g ⊢ ( 𝐶 ∈ V → 𝐶 ∈ { 𝐶 , 𝐷 } )
11 9 10 syl ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 ∈ { 𝐶 , 𝐷 } )
12 eleq2 ⊢ ( { 𝐴 } = { 𝐶 , 𝐷 } → ( 𝐶 ∈ { 𝐴 } ↔ 𝐶 ∈ { 𝐶 , 𝐷 } ) )
13 11 12 syl5ibrcom ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( { 𝐴 } = { 𝐶 , 𝐷 } → 𝐶 ∈ { 𝐴 } ) )
14 elsni ⊢ ( 𝐶 ∈ { 𝐴 } → 𝐶 = 𝐴 )
15 14 eqcomd ⊢ ( 𝐶 ∈ { 𝐴 } → 𝐴 = 𝐶 )
16 13 15 syl6 ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( { 𝐴 } = { 𝐶 , 𝐷 } → 𝐴 = 𝐶 ) )
17 id ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ )
18 dfopg ⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ⟨ 𝐶 , 𝐷 ⟩ = { { 𝐶 } , { 𝐶 , 𝐷 } } )
19 8 18 syl ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐶 , 𝐷 ⟩ = { { 𝐶 } , { 𝐶 , 𝐷 } } )
20 17 19 eleqtrd ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 } ∈ { { 𝐶 } , { 𝐶 , 𝐷 } } )
21 elpri ⊢ ( { 𝐴 } ∈ { { 𝐶 } , { 𝐶 , 𝐷 } } → ( { 𝐴 } = { 𝐶 } ∨ { 𝐴 } = { 𝐶 , 𝐷 } ) )
22 20 21 syl ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( { 𝐴 } = { 𝐶 } ∨ { 𝐴 } = { 𝐶 , 𝐷 } ) )
23 7 16 22 mpjaod ⊢ ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )
24 5 23 syl ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )