# 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 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )