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

Theorem opth 4769
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 4768 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
41, 2opi1 4762 . . . . . . 7 {𝐴} ∈ ⟨𝐴, 𝐵
5 id 22 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
64, 5syl5eleq 2598 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7 oprcl 4263 . . . . . 6 ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
86, 7syl 17 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
98simprd 477 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
103opeq1d 4244 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
1110, 5eqtr3d 2550 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
128simpld 473 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13 dfopg 4236 . . . . . . . 8 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1412, 2, 13sylancl 692 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1511, 14eqtr3d 2550 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16 dfopg 4236 . . . . . . 7 ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
178, 16syl 17 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
1815, 17eqtr3d 2550 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19 prex 4735 . . . . . 6 {𝐶, 𝐵} ∈ V
20 prex 4735 . . . . . 6 {𝐶, 𝐷} ∈ V
2119, 20preqr2 4220 . . . . 5 ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
2218, 21syl 17 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23 preq2 4116 . . . . . . 7 (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
2423eqeq2d 2524 . . . . . 6 (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25 eqeq2 2525 . . . . . 6 (𝑥 = 𝐷 → (𝐵 = 𝑥𝐵 = 𝐷))
2624, 25imbi12d 332 . . . . 5 (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27 vex 3080 . . . . . 6 𝑥 ∈ V
282, 27preqr2 4220 . . . . 5 ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
2926, 28vtoclg 3143 . . . 4 (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
309, 22, 29sylc 62 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
313, 30jca 552 . 2 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶𝐵 = 𝐷))
32 opeq12 4240 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3331, 32impbii 197 1 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  Vcvv 3077  {csn 4028  {cpr 4030  cop 4034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035
This theorem is referenced by:  opthg  4770  otth2  4776  copsexg  4780  copsex4g  4783  opcom  4788  moop2  4789  opelopabsbALT  4803  ralxpf  5082  cnvcnvsn  5420  funopg  5726  tpres  6253  oprabv  6483  xpopth  6978  eqop  6979  opiota  6998  soxp  7057  fnwelem  7059  xpdom2  7820  xpf1o  7887  unxpdomlem2  7930  unxpdomlem3  7931  xpwdomg  8253  fseqenlem1  8610  iundom2g  9121  eqresr  9717  cnref1o  11573  hashfun  12953  fsumcom2  14220  fsumcom2OLD  14221  fprodcom2  14426  fprodcom2OLD  14427  qredeu  15090  qnumdenbi  15170  crth  15203  prmreclem3  15348  imasaddfnlem  15907  dprd2da  18175  dprd2d2  18177  ucnima  21802  numclwlk1lem2f1  26363  br8d  28594  xppreima2  28622  aciunf1lem  28636  ofpreima  28640  erdszelem9  30284  msubff1  30556  mvhf1  30559  brtp  30738  br8  30745  br6  30746  br4  30747  brsegle  31224  poimirlem4  32477  poimirlem9  32482  f1opr  32583  dib1dim  35366  diclspsn  35395  dihopelvalcpre  35449  dihmeetlem4preN  35507  dihmeetlem13N  35520  dih1dimatlem  35530  dihatlat  35535  pellexlem3  36307  pellex  36311  snhesn  37001  opelopab4  37689  propssopi  40234  funsndifnop  40255  av-numclwlk1lem2f1  41633
  Copyright terms: Public domain W3C validator