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 ⊢ A ∈ V
opth1.2 ⊢ B ∈ V
Assertion opth1 ⊢ A B = C D → A = C

Proof

Step Hyp Ref Expression
1 opth1.1 ⊢ A ∈ V
2 opth1.2 ⊢ B ∈ V
3 1 2 opi1 ⊢ A ∈ A B
4 id ⊢ A B = C D → A B = C D
5 3 4 eleqtrid ⊢ A B = C D → A ∈ C D
6 1 sneqr ⊢ A = C → A = C
7 6 a1i ⊢ A ∈ C D → A = C → A = C
8 oprcl ⊢ A ∈ C D → C ∈ V ∧ D ∈ V
9 8 simpld ⊢ A ∈ C D → C ∈ V
10 prid1g ⊢ C ∈ V → C ∈ C D
11 9 10 syl ⊢ A ∈ C D → C ∈ C D
12 eleq2 ⊢ A = C D → C ∈ A ↔ C ∈ C D
13 11 12 syl5ibrcom ⊢ A ∈ C D → A = C D → C ∈ A
14 elsni ⊢ C ∈ A → C = A
15 14 eqcomd ⊢ C ∈ A → A = C
16 13 15 syl6 ⊢ A ∈ C D → A = C D → A = C
17 id ⊢ A ∈ C D → A ∈ C D
18 dfopg ⊢ C ∈ V ∧ D ∈ V → C D = C C D
19 8 18 syl ⊢ A ∈ C D → C D = C C D
20 17 19 eleqtrd ⊢ A ∈ C D → A ∈ C C D
21 elpri ⊢ A ∈ C C D → A = C ∨ A = C D
22 20 21 syl ⊢ A ∈ C D → A = C ∨ A = C D
23 7 16 22 mpjaod ⊢ A ∈ C D → A = C
24 5 23 syl ⊢ A B = C D → A = C