Theorem opth 5459

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 5458	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
4	1, 2	opi1 5451	. . . . . . 7 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
5		id 23	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
6	4, 5	eleqtrid 2875	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7		oprcl 4868	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
8	6, 7	syl 18	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simprd 500	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
10	3	opeq1d 4848	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
11	10, 5	eqtr3d 2806	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
12	8	simpld 499	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13		dfopg 4840	. . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
14	12, 2, 13	sylancl 597	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
15	11, 14	eqtr3d 2806	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16		dfopg 4840	. . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
17	8, 16	syl 18	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
18	15, 17	eqtr3d 2806	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19		prex 5410	. . . . . 6 ⊢ {𝐶, 𝐵} ∈ V
20		prex 5410	. . . . . 6 ⊢ {𝐶, 𝐷} ∈ V
21	19, 20	preqr2 4818	. . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
22	18, 21	syl 18	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23		preq2 4705	. . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
24	23	eqeq2d 2780	. . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25		eqeq2 2781	. . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷))
26	24, 25	imbi12d 347	. . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27		vex 3467	. . . . . 6 ⊢ 𝑥 ∈ V
28	2, 27	preqr2 4818	. . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
29	26, 28	vtoclg 3531	. . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
30	9, 22, 29	sylc 66	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
31	3, 30	jca 520	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
32		opeq12 4844	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
33	31, 32	impbii 212	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594  {cpr 4596  ⟨cop 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is referenced by:  opthg  5460  otth2  5466  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  copsex2g  5477  copsex4g  5479  opcom  5485  moop2  5486  propssopi  5492  brtp  5508  vopelopabsb  5514  brab2d  5523  ralxpf  5833  cnvopab  6138  cnvcnvsn  6221  opreu2reurex  6296  funopg  6571  funsndifnop  7149  tpres  7200  f1opr  7467  oprabv  7471  xpopth  8027  eqop  8028  opiota  8056  soxp  8125  fnwelem  8127  xpdom2  9060  xpf1o  9127  unxpdomlem2  9217  unxpdomlem3  9218  xpwdomg  9547  djulf1o  9898  djurf1o  9899  fseqenlem1  10008  iundom2g  10524  eqresr  11122  cnref1o  13009  hashfun  14474  fsumcom2  15825  fprodcom2  16038  qredeu  16716  qnumdenbi  16803  crth  16837  prmreclem3  16978  imasaddfnlem  17582  fnpr2ob  17612  dprd2da  20114  dprd2d2  20116  rngqiprngimf1  21411  ucnima  24406  numclwwlk1lem2f1  30649  br8d  32894  xppreima2  32937  aciunf1lem  32948  ofpreima  32951  erdszelem9  35590  goeleq12bg  35740  gonanegoal  35743  gonan0  35783  goaln0  35784  gonarlem  35785  gonar  35786  goalrlem  35787  goalr  35788  fmla0disjsuc  35789  fmlasucdisj  35790  satffunlem  35792  satffunlem1lem1  35793  satffunlem2lem1  35795  msubff1  35947  mvhf1  35950  br8  36147  br6  36148  br4  36149  brsegle  36499  nmulprop  36581  copsex2gd  37670  copsex2b  37672  poimirlem4  38163  poimirlem9  38168  dib1dim  41829  diclspsn  41858  dihopelvalcpre  41912  dihmeetlem4preN  41970  dihmeetlem13N  41983  dih1dimatlem  41993  dihatlat  41998  pellexlem3  43450  pellex  43454  snhesn  44404  opelopab4  45152  ichnreuop  48110  ichreuopeq  48111  gpgedg2ov  48720  gpgedg2iv  48721  pgnioedg1  48762  pgnioedg2  48763  pgnioedg3  48764  pgnioedg4  48765  pgnioedg5  48766  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  pgnbgreunbgrlem2lem3  48770  pgnbgreunbgrlem5lem1  48774  pgnbgreunbgrlem5lem2  48775  pgnbgreunbgrlem5lem3  48776  rrx2xpref1o  49383  brab2dd  49491  idfudiag1  50188