Theorem opth 1898

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 is not required to be a set due to a peculiarity of our specific ordered pair definition.

Hypotheses

Ref	Expression
opth.1	⊢ A ∈ V
opth.2	⊢ B ∈ V
opth.3	⊢ D ∈ V

Assertion

Ref	Expression
opth	⊢ (⟨A, B⟩ = ⟨C, D⟩ ↔ (A = C ∧ B = D))

Proof of Theorem opth

Step	Hyp	Ref	Expression
1		opi1 1895	. . . . . . 7 ⊢ {C} ∈ ⟨C, D⟩
2		eleq2 1150	. . . . . . 7 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → ({C} ∈ ⟨A, B⟩ ↔ {C} ∈ ⟨C, D⟩))
3	1, 2	mpbiri 169	. . . . . 6 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → {C} ∈ ⟨A, B⟩)
4		snex 1859	. . . . . . 7 ⊢ {C} ∈ V
5	4	elop 1894	. . . . . 6 ⊢ ({C} ∈ ⟨A, B⟩ ↔ ({C} = {A} ∨ {C} = {A, B}))
6	3, 5	sylib 173	. . . . 5 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → ({C} = {A} ∨ {C} = {A, B}))
7		opth.1	. . . . . . . 8 ⊢ A ∈ V
8	7	snid 1830	. . . . . . 7 ⊢ A ∈ {A}
9		eleq2 1150	. . . . . . 7 ⊢ ({C} = {A} → (A ∈ {C} ↔ A ∈ {A}))
10	8, 9	mpbiri 169	. . . . . 6 ⊢ ({C} = {A} → A ∈ {C})
11	7	pri1 1841	. . . . . . 7 ⊢ A ∈ {A, B}
12		eleq2 1150	. . . . . . 7 ⊢ ({C} = {A, B} → (A ∈ {C} ↔ A ∈ {A, B}))
13	11, 12	mpbiri 169	. . . . . 6 ⊢ ({C} = {A, B} → A ∈ {C})
14	10, 13	jaoi 275	. . . . 5 ⊢ (({C} = {A} ∨ {C} = {A, B}) → A ∈ {C})
15	6, 14	syl 12	. . . 4 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → A ∈ {C})
16	7	elsnc 1826	. . . 4 ⊢ (A ∈ {C} ↔ A = C)
17	15, 16	sylib 173	. . 3 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → A = C)
18		cleq1 1107	. . . . 5 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → (⟨A, B⟩ = ⟨C, B⟩ ↔ ⟨C, D⟩ = ⟨C, B⟩))
19		opeq1 1876	. . . . 5 ⊢ (A = C → ⟨A, B⟩ = ⟨C, B⟩)
20	18, 19	syl5bi 183	. . . 4 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → (A = C → ⟨C, D⟩ = ⟨C, B⟩))
21		df-op 1815	. . . . . . 7 ⊢ ⟨C, D⟩ = {{C}, {C, D}}
22		df-op 1815	. . . . . . 7 ⊢ ⟨C, B⟩ = {{C}, {C, B}}
23	21, 22	cleq12i 1114	. . . . . 6 ⊢ (⟨C, D⟩ = ⟨C, B⟩ ↔ {{C}, {C, D}} = {{C}, {C, B}})
24		prex 1892	. . . . . . 7 ⊢ {C, D} ∈ V
25		prex 1892	. . . . . . 7 ⊢ {C, B} ∈ V
26	24, 25	prer2 1873	. . . . . 6 ⊢ ({{C}, {C, D}} = {{C}, {C, B}} → {C, D} = {C, B})
27	23, 26	sylbi 174	. . . . 5 ⊢ (⟨C, D⟩ = ⟨C, B⟩ → {C, D} = {C, B})
28		opth.3	. . . . . . 7 ⊢ D ∈ V
29		opth.2	. . . . . . 7 ⊢ B ∈ V
30	28, 29	prer2 1873	. . . . . 6 ⊢ ({C, D} = {C, B} → D = B)
31	30	cleqcomd 1106	. . . . 5 ⊢ ({C, D} = {C, B} → B = D)
32	27, 31	syl 12	. . . 4 ⊢ (⟨C, D⟩ = ⟨C, B⟩ → B = D)
33	20, 32	syl6 23	. . 3 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → (A = C → B = D))
34	17, 33	jcai 237	. 2 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → (A = C ∧ B = D))
35		opeq12 1878	. 2 ⊢ ((A = C ∧ B = D) → ⟨A, B⟩ = ⟨C, D⟩)
36	34, 35	impbi 139	1 ⊢ (⟨A, B⟩ = ⟨C, D⟩ ↔ (A = C ∧ B = D))

Syntax hints:   ↔ wb 127   ∨ wo 195   ∧ wa 196   = wceq 1091   ∈ wcel 1092  Vcvv 1348  {csn 1808  {cpr 1809  ⟨cop 1810

This theorem is referenced by:  opthg 1899  eqvinop 1901  copsexg 1902  opth2 1909  opabid 2099  opelxp 2452  cnvsn 2636  funsn 2690  fsn 2895  xpdom2 3345  xpmapenlem4 3394  aceq5lem4 3561  eqresr 4049  ltresr 4052  axrecex 4079  axi2m1 4082  xpnnen 4927

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815

metamath.org