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

Theorem opth 5072
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 5071 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
41, 2opi1 5064 . . . . . . 7 {𝐴} ∈ ⟨𝐴, 𝐵
5 id 22 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
64, 5syl5eleq 2856 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7 oprcl 4565 . . . . . 6 ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
86, 7syl 17 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
98simprd 483 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
103opeq1d 4545 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
1110, 5eqtr3d 2807 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
128simpld 482 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13 dfopg 4537 . . . . . . . 8 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1412, 2, 13sylancl 574 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1511, 14eqtr3d 2807 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16 dfopg 4537 . . . . . . 7 ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
178, 16syl 17 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
1815, 17eqtr3d 2807 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19 prex 5037 . . . . . 6 {𝐶, 𝐵} ∈ V
20 prex 5037 . . . . . 6 {𝐶, 𝐷} ∈ V
2119, 20preqr2 4512 . . . . 5 ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
2218, 21syl 17 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23 preq2 4405 . . . . . . 7 (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
2423eqeq2d 2781 . . . . . 6 (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25 eqeq2 2782 . . . . . 6 (𝑥 = 𝐷 → (𝐵 = 𝑥𝐵 = 𝐷))
2624, 25imbi12d 333 . . . . 5 (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27 vex 3354 . . . . . 6 𝑥 ∈ V
282, 27preqr2 4512 . . . . 5 ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
2926, 28vtoclg 3417 . . . 4 (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
309, 22, 29sylc 65 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
313, 30jca 501 . 2 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶𝐵 = 𝐷))
32 opeq12 4541 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3331, 32impbii 199 1 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  Vcvv 3351  {csn 4316  {cpr 4318  cop 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323
This theorem is referenced by:  opthg  5073  otth2  5079  copsexg  5083  copsex4g  5086  opcom  5092  moop2  5093  propssopi  5101  opelopabsbALT  5117  ralxpf  5407  cnvcnvsn  5754  funopg  6065  funsndifnop  6559  tpres  6610  oprabv  6850  xpopth  7356  eqop  7357  opiota  7378  soxp  7441  fnwelem  7443  xpdom2  8211  xpf1o  8278  unxpdomlem2  8321  unxpdomlem3  8322  xpwdomg  8646  djulf1o  8938  djurf1o  8939  fseqenlem1  9047  iundom2g  9564  eqresr  10160  cnref1o  12030  hashfun  13426  fsumcom2  14713  fprodcom2  14921  qredeu  15579  qnumdenbi  15659  crth  15690  prmreclem3  15829  imasaddfnlem  16396  dprd2da  18649  dprd2d2  18651  ucnima  22305  numclwwlk1lem2f1  27543  br8d  29760  xppreima2  29790  aciunf1lem  29802  ofpreima  29805  erdszelem9  31519  msubff1  31791  mvhf1  31794  brtp  31977  br8  31984  br6  31985  br4  31986  brsegle  32552  poimirlem4  33746  poimirlem9  33751  f1opr  33851  dib1dim  36975  diclspsn  37004  dihopelvalcpre  37058  dihmeetlem4preN  37116  dihmeetlem13N  37129  dih1dimatlem  37139  dihatlat  37144  pellexlem3  37921  pellex  37925  snhesn  38606  opelopab4  39292
  Copyright terms: Public domain W3C validator