Theorem opth 5452

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 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)

Hypotheses

Ref	Expression
opth1.1	⊢ 𝐴 ∈ V
opth1.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opth	⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Proof of Theorem opth

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opth1.1	. . . 4 ⊢ 𝐴 ∈ V
2		opth1.2	. . . 4 ⊢ 𝐵 ∈ V
3	1, 2	opth1 5451	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
4	1, 2	opi1 5444	. . . . . . 7 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
5		id 23	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
6	4, 5	eleqtrid 2866	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7		oprcl 4859	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
8	6, 7	syl 18	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simprd 501	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
10	3	opeq1d 4839	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
11	10, 5	eqtr3d 2797	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
12	8	simpld 500	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13		dfopg 4831	. . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
14	12, 2, 13	sylancl 598	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
15	11, 14	eqtr3d 2797	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16		dfopg 4831	. . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
17	8, 16	syl 18	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
18	15, 17	eqtr3d 2797	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19		prex 5403	. . . . . 6 ⊢ {𝐶, 𝐵} ∈ V
20		prex 5403	. . . . . 6 ⊢ {𝐶, 𝐷} ∈ V
21	19, 20	preqr2 4809	. . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
22	18, 21	syl 18	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23		preq2 4695	. . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
24	23	eqeq2d 2771	. . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25		eqeq2 2772	. . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷))
26	24, 25	imbi12d 347	. . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
28	2, 27	preqr2 4809	. . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
29	26, 28	vtoclg 3517	. . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
30	9, 22, 29	sylc 66	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
31	3, 30	jca 521	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
32		opeq12 4835	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
33	31, 32	impbii 212	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450  {csn 4584  {cpr 4586  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  opthg  5453  otth2  5459  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  copsex2g  5470  copsex4g  5472  opcom  5478  moop2  5479  propssopi  5485  brtp  5501  vopelopabsb  5507  brab2d  5516  ralxpf  5826  cnvopab  6131  cnvcnvsn  6215  opreu2reurex  6292  funopg  6568  funsndifnop  7149  tpres  7201  f1opr  7470  oprabv  7474  xpopth  8028  eqop  8029  opiota  8057  soxp  8128  fnwelem  8130  xpdom2  9073  xpf1o  9140  unxpdomlem2  9230  unxpdomlem3  9231  xpwdomg  9560  djulf1o  9920  djurf1o  9921  fseqenlem1  10030  iundom2g  10551  eqresr  11149  cnref1o  13038  hashfun  14505  fsumcom2  15863  fprodcom2  16074  qredeu  16751  qnumdenbi  16838  crth  16872  prmreclem3  17013  imasaddfnlem  17617  fnpr2ob  17647  dprd2da  20174  dprd2d2  20176  rngqiprngimf1  21506  ucnima  24509  numclwwlk1lem2f1  30840  br8d  33084  xppreima2  33127  aciunf1lem  33138  ofpreima  33141  erdszelem9  35781  goeleq12bg  35931  gonanegoal  35934  gonan0  35974  goaln0  35975  gonarlem  35976  gonar  35977  goalrlem  35978  goalr  35979  fmla0disjsuc  35980  fmlasucdisj  35981  satffunlem  35983  satffunlem1lem1  35984  satffunlem2lem1  35986  msubff1  36138  mvhf1  36141  br8  36338  br6  36339  br4  36340  brsegle  36691  nmulprop  36773  copsex2gd  37893  copsex2b  37895  poimirlem4  38376  poimirlem9  38381  dib1dim  42041  diclspsn  42070  dihopelvalcpre  42124  dihmeetlem4preN  42182  dihmeetlem13N  42195  dih1dimatlem  42205  dihatlat  42210  pellexlem3  43675  pellex  43679  snhesn  44629  opelopab4  45377  ichnreuop  48375  ichreuopeq  48376  gpgedg2ov  48985  gpgedg2iv  48986  pgnioedg1  49027  pgnioedg2  49028  pgnioedg3  49029  pgnioedg4  49030  pgnioedg5  49031  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem2lem3  49035  pgnbgreunbgrlem5lem1  49039  pgnbgreunbgrlem5lem2  49040  pgnbgreunbgrlem5lem3  49041  rrx2xpref1o  49651  brab2dd  49759  idfudiag1  50454