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

Metamath Proof Explorer

Theorem opth

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of TakeutiZaring p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses opth1.1 ⊢ A ∈ V
opth1.2 ⊢ B ∈ V
Assertion opth ⊢ A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opth1.1 ⊢ A ∈ V
2 opth1.2 ⊢ B ∈ V
3 1 2 opth1 ⊢ A B = C D → A = C
4 1 2 opi1 ⊢ A ∈ A B
5 id ⊢ A B = C D → A B = C D
6 4 5 eleqtrid ⊢ A B = C D → A ∈ C D
7 oprcl ⊢ A ∈ C D → C ∈ V ∧ D ∈ V
8 6 7 syl ⊢ A B = C D → C ∈ V ∧ D ∈ V
9 8 simprd ⊢ A B = C D → D ∈ V
10 3 opeq1d ⊢ A B = C D → A B = C B
11 10 5 eqtr3d ⊢ A B = C D → C B = C D
12 8 simpld ⊢ A B = C D → C ∈ V
13 dfopg ⊢ C ∈ V ∧ B ∈ V → C B = C C B
14 12 2 13 sylancl ⊢ A B = C D → C B = C C B
15 11 14 eqtr3d ⊢ A B = C D → C D = C C B
16 dfopg ⊢ C ∈ V ∧ D ∈ V → C D = C C D
17 8 16 syl ⊢ A B = C D → C D = C C D
18 15 17 eqtr3d ⊢ A B = C D → C C B = C C D
19 prex ⊢ C B ∈ V
20 prex ⊢ C D ∈ V
21 19 20 preqr2 ⊢ C C B = C C D → C B = C D
22 18 21 syl ⊢ A B = C D → C B = C D
23 preq2 ⊢ x = D → C x = C D
24 23 eqeq2d ⊢ x = D → C B = C x ↔ C B = C D
25 eqeq2 ⊢ x = D → B = x ↔ B = D
26 24 25 imbi12d ⊢ x = D → C B = C x → B = x ↔ C B = C D → B = D
27 vex ⊢ x ∈ V
28 2 27 preqr2 ⊢ C B = C x → B = x
29 26 28 vtoclg ⊢ D ∈ V → C B = C D → B = D
30 9 22 29 sylc ⊢ A B = C D → B = D
31 3 30 jca ⊢ A B = C D → A = C ∧ B = D
32 opeq12 ⊢ A = C ∧ B = D → A B = C D
33 31 32 impbii ⊢ A B = C D ↔ A = C ∧ B = D