Theorem opth 5475

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 5474	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
4	1, 2	opi1 5467	. . . . . . 7 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
5		id 22	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
6	4, 5	eleqtrid 2840	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7		oprcl 4898	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
8	6, 7	syl 17	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simprd 497	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
10	3	opeq1d 4878	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
11	10, 5	eqtr3d 2775	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
12	8	simpld 496	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13		dfopg 4870	. . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
14	12, 2, 13	sylancl 587	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
15	11, 14	eqtr3d 2775	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16		dfopg 4870	. . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
17	8, 16	syl 17	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
18	15, 17	eqtr3d 2775	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19		prex 5431	. . . . . 6 ⊢ {𝐶, 𝐵} ∈ V
20		prex 5431	. . . . . 6 ⊢ {𝐶, 𝐷} ∈ V
21	19, 20	preqr2 4849	. . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
22	18, 21	syl 17	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23		preq2 4737	. . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
24	23	eqeq2d 2744	. . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25		eqeq2 2745	. . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷))
26	24, 25	imbi12d 345	. . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27		vex 3479	. . . . . 6 ⊢ 𝑥 ∈ V
28	2, 27	preqr2 4849	. . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
29	26, 28	vtoclg 3556	. . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
30	9, 22, 29	sylc 65	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
31	3, 30	jca 513	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
32		opeq12 4874	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
33	31, 32	impbii 208	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4627  {cpr 4629  ⟨cop 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634

This theorem is referenced by:  opthg  5476  otth2  5482  copsexgw  5489  copsexg  5490  copsex2g  5492  copsex4g  5494  opcom  5500  moop2  5501  propssopi  5507  brtp  5522  vopelopabsb  5528  ralxpf  5844  cnvcnvsn  6215  opreu2reurex  6290  funopg  6579  funsndifnop  7144  tpres  7197  f1opr  7460  oprabv  7464  xpopth  8011  eqop  8012  opiota  8040  soxp  8110  fnwelem  8112  xpdom2  9063  xpf1o  9135  unxpdomlem2  9247  unxpdomlem3  9248  xpwdomg  9576  djulf1o  9903  djurf1o  9904  fseqenlem1  10015  iundom2g  10531  eqresr  11128  cnref1o  12965  hashfun  14393  fsumcom2  15716  fprodcom2  15924  qredeu  16591  qnumdenbi  16676  crth  16707  prmreclem3  16847  imasaddfnlem  17470  fnpr2ob  17500  dprd2da  19904  dprd2d2  19906  ucnima  23768  numclwwlk1lem2f1  29590  br8d  31817  xppreima2  31854  aciunf1lem  31865  ofpreima  31868  erdszelem9  34128  goeleq12bg  34278  gonanegoal  34281  gonan0  34321  goaln0  34322  gonarlem  34323  gonar  34324  goalrlem  34325  goalr  34326  fmla0disjsuc  34327  fmlasucdisj  34328  satffunlem  34330  satffunlem1lem1  34331  satffunlem2lem1  34333  msubff1  34485  mvhf1  34488  br8  34664  br6  34665  br4  34666  brsegle  35018  copsex2b  35959  poimirlem4  36430  poimirlem9  36435  dib1dim  39974  diclspsn  40003  dihopelvalcpre  40057  dihmeetlem4preN  40115  dihmeetlem13N  40128  dih1dimatlem  40138  dihatlat  40143  pellexlem3  41502  pellex  41506  snhesn  42470  opelopab4  43245  ichnreuop  46075  ichreuopeq  46076  rngqiprngimf1  46714  rrx2xpref1o  47306