# 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}\in \mathrm{V}$
opth1.2 ${⊢}{B}\in \mathrm{V}$
Assertion opth ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {B}={D}\right)$

### Proof

Step Hyp Ref Expression
1 opth1.1 ${⊢}{A}\in \mathrm{V}$
2 opth1.2 ${⊢}{B}\in \mathrm{V}$
3 1 2 opth1 ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to {A}={C}$
4 1 2 opi1 ${⊢}\left\{{A}\right\}\in ⟨{A},{B}⟩$
5 id ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{A},{B}⟩=⟨{C},{D}⟩$
6 4 5 eleqtrid ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to \left\{{A}\right\}\in ⟨{C},{D}⟩$
7 oprcl ${⊢}\left\{{A}\right\}\in ⟨{C},{D}⟩\to \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)$
8 6 7 syl ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)$
9 8 simprd ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to {D}\in \mathrm{V}$
10 3 opeq1d ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{A},{B}⟩=⟨{C},{B}⟩$
11 10 5 eqtr3d ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{C},{B}⟩=⟨{C},{D}⟩$
12 8 simpld ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to {C}\in \mathrm{V}$
13 dfopg ${⊢}\left({C}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to ⟨{C},{B}⟩=\left\{\left\{{C}\right\},\left\{{C},{B}\right\}\right\}$
14 12 2 13 sylancl ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{C},{B}⟩=\left\{\left\{{C}\right\},\left\{{C},{B}\right\}\right\}$
15 11 14 eqtr3d ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{C},{D}⟩=\left\{\left\{{C}\right\},\left\{{C},{B}\right\}\right\}$
16 dfopg ${⊢}\left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\to ⟨{C},{D}⟩=\left\{\left\{{C}\right\},\left\{{C},{D}\right\}\right\}$
17 8 16 syl ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to ⟨{C},{D}⟩=\left\{\left\{{C}\right\},\left\{{C},{D}\right\}\right\}$
18 15 17 eqtr3d ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to \left\{\left\{{C}\right\},\left\{{C},{B}\right\}\right\}=\left\{\left\{{C}\right\},\left\{{C},{D}\right\}\right\}$
19 prex ${⊢}\left\{{C},{B}\right\}\in \mathrm{V}$
20 prex ${⊢}\left\{{C},{D}\right\}\in \mathrm{V}$
21 19 20 preqr2 ${⊢}\left\{\left\{{C}\right\},\left\{{C},{B}\right\}\right\}=\left\{\left\{{C}\right\},\left\{{C},{D}\right\}\right\}\to \left\{{C},{B}\right\}=\left\{{C},{D}\right\}$
22 18 21 syl ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to \left\{{C},{B}\right\}=\left\{{C},{D}\right\}$
23 preq2 ${⊢}{x}={D}\to \left\{{C},{x}\right\}=\left\{{C},{D}\right\}$
24 23 eqeq2d ${⊢}{x}={D}\to \left(\left\{{C},{B}\right\}=\left\{{C},{x}\right\}↔\left\{{C},{B}\right\}=\left\{{C},{D}\right\}\right)$
25 eqeq2 ${⊢}{x}={D}\to \left({B}={x}↔{B}={D}\right)$
26 24 25 imbi12d ${⊢}{x}={D}\to \left(\left(\left\{{C},{B}\right\}=\left\{{C},{x}\right\}\to {B}={x}\right)↔\left(\left\{{C},{B}\right\}=\left\{{C},{D}\right\}\to {B}={D}\right)\right)$
27 vex ${⊢}{x}\in \mathrm{V}$
28 2 27 preqr2 ${⊢}\left\{{C},{B}\right\}=\left\{{C},{x}\right\}\to {B}={x}$
29 26 28 vtoclg ${⊢}{D}\in \mathrm{V}\to \left(\left\{{C},{B}\right\}=\left\{{C},{D}\right\}\to {B}={D}\right)$
30 9 22 29 sylc ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to {B}={D}$
31 3 30 jca ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩\to \left({A}={C}\wedge {B}={D}\right)$
32 opeq12 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to ⟨{A},{B}⟩=⟨{C},{D}⟩$
33 31 32 impbii ${⊢}⟨{A},{B}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {B}={D}\right)$