MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opth Structured version   Visualization version   GIF version

Theorem opth 5479
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.
StepHypRef Expression
1 opth1.1 . . . 4 𝐴 ∈ V
2 opth1.2 . . . 4 𝐵 ∈ V
31, 2opth1 5478 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
41, 2opi1 5471 . . . . . . 7 {𝐴} ∈ ⟨𝐴, 𝐵
5 id 22 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
64, 5eleqtrid 2846 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7 oprcl 4897 . . . . . 6 ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
86, 7syl 17 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
98simprd 495 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
103opeq1d 4877 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
1110, 5eqtr3d 2778 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
128simpld 494 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13 dfopg 4869 . . . . . . . 8 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1412, 2, 13sylancl 586 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1511, 14eqtr3d 2778 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16 dfopg 4869 . . . . . . 7 ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
178, 16syl 17 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
1815, 17eqtr3d 2778 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19 prex 5435 . . . . . 6 {𝐶, 𝐵} ∈ V
20 prex 5435 . . . . . 6 {𝐶, 𝐷} ∈ V
2119, 20preqr2 4847 . . . . 5 ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
2218, 21syl 17 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23 preq2 4732 . . . . . . 7 (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
2423eqeq2d 2747 . . . . . 6 (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25 eqeq2 2748 . . . . . 6 (𝑥 = 𝐷 → (𝐵 = 𝑥𝐵 = 𝐷))
2624, 25imbi12d 344 . . . . 5 (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27 vex 3483 . . . . . 6 𝑥 ∈ V
282, 27preqr2 4847 . . . . 5 ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
2926, 28vtoclg 3553 . . . 4 (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
309, 22, 29sylc 65 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
313, 30jca 511 . 2 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶𝐵 = 𝐷))
32 opeq12 4873 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3331, 32impbii 209 1 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  Vcvv 3479  {csn 4624  {cpr 4626  cop 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631
This theorem is referenced by:  opthg  5480  otth2  5486  copsexgw  5493  copsexg  5494  copsex2g  5496  copsex4g  5498  opcom  5504  moop2  5505  propssopi  5511  brtp  5526  vopelopabsb  5532  ralxpf  5855  cnvopab  6155  cnvcnvsn  6237  opreu2reurex  6312  funopg  6598  funsndifnop  7169  tpres  7219  f1opr  7487  oprabv  7491  xpopth  8051  eqop  8052  opiota  8080  soxp  8150  fnwelem  8152  xpdom2  9103  xpf1o  9175  unxpdomlem2  9283  unxpdomlem3  9284  xpwdomg  9621  djulf1o  9948  djurf1o  9949  fseqenlem1  10060  iundom2g  10576  eqresr  11173  cnref1o  13023  hashfun  14472  fsumcom2  15806  fprodcom2  16016  qredeu  16691  qnumdenbi  16777  crth  16811  prmreclem3  16952  imasaddfnlem  17569  fnpr2ob  17599  dprd2da  20058  dprd2d2  20060  rngqiprngimf1  21302  ucnima  24280  numclwwlk1lem2f1  30366  brab2d  32608  br8d  32611  xppreima2  32650  aciunf1lem  32661  ofpreima  32664  erdszelem9  35182  goeleq12bg  35332  gonanegoal  35335  gonan0  35375  goaln0  35376  gonarlem  35377  gonar  35378  goalrlem  35379  goalr  35380  fmla0disjsuc  35381  fmlasucdisj  35382  satffunlem  35384  satffunlem1lem1  35385  satffunlem2lem1  35387  msubff1  35539  mvhf1  35542  br8  35734  br6  35735  br4  35736  brsegle  36087  copsex2b  37119  poimirlem4  37609  poimirlem9  37614  dib1dim  41145  diclspsn  41174  dihopelvalcpre  41228  dihmeetlem4preN  41286  dihmeetlem13N  41299  dih1dimatlem  41309  dihatlat  41314  pellexlem3  42820  pellex  42824  snhesn  43777  opelopab4  44549  ichnreuop  47432  ichreuopeq  47433  rrx2xpref1o  48612  brab2dd  48714
  Copyright terms: Public domain W3C validator