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