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

Theorem opth 5341
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 5340 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
41, 2opi1 5333 . . . . . . 7 {𝐴} ∈ ⟨𝐴, 𝐵
5 id 22 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
64, 5eleqtrid 2918 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
7 oprcl 4802 . . . . . 6 ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
86, 7syl 17 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
98simprd 499 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V)
103opeq1d 4782 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
1110, 5eqtr3d 2858 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
128simpld 498 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
13 dfopg 4774 . . . . . . . 8 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1412, 2, 13sylancl 589 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}})
1511, 14eqtr3d 2858 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}})
16 dfopg 4774 . . . . . . 7 ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
178, 16syl 17 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
1815, 17eqtr3d 2858 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}})
19 prex 5306 . . . . . 6 {𝐶, 𝐵} ∈ V
20 prex 5306 . . . . . 6 {𝐶, 𝐷} ∈ V
2119, 20preqr2 4753 . . . . 5 ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})
2218, 21syl 17 . . . 4 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷})
23 preq2 4643 . . . . . . 7 (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷})
2423eqeq2d 2832 . . . . . 6 (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
25 eqeq2 2833 . . . . . 6 (𝑥 = 𝐷 → (𝐵 = 𝑥𝐵 = 𝐷))
2624, 25imbi12d 348 . . . . 5 (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)))
27 vex 3474 . . . . . 6 𝑥 ∈ V
282, 27preqr2 4753 . . . . 5 ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥)
2926, 28vtoclg 3544 . . . 4 (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
309, 22, 29sylc 65 . . 3 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷)
313, 30jca 515 . 2 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶𝐵 = 𝐷))
32 opeq12 4778 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3331, 32impbii 212 1 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  Vcvv 3471  {csn 4540  {cpr 4542  cop 4546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547
This theorem is referenced by:  opthg  5342  otth2  5348  copsexgw  5354  copsexg  5355  copsex4g  5358  opcom  5364  moop2  5365  propssopi  5371  opelopabsbALT  5389  ralxpf  5690  cnvcnvsn  6049  opreu2reurex  6118  funopg  6362  funsndifnop  6886  tpres  6936  f1opr  7184  oprabv  7188  xpopth  7705  eqop  7706  opiota  7732  soxp  7798  fnwelem  7800  xpdom2  8587  xpf1o  8655  unxpdomlem2  8699  unxpdomlem3  8700  xpwdomg  9025  djulf1o  9317  djurf1o  9318  fseqenlem1  9427  iundom2g  9939  eqresr  10536  cnref1o  12362  hashfun  13782  fsumcom2  15108  fprodcom2  15317  qredeu  15979  qnumdenbi  16061  crth  16092  prmreclem3  16231  imasaddfnlem  16779  fnpr2ob  16809  dprd2da  19142  dprd2d2  19144  ucnima  22865  numclwwlk1lem2f1  28120  br8d  30347  xppreima2  30381  aciunf1lem  30393  ofpreima  30396  erdszelem9  32453  goeleq12bg  32603  gonanegoal  32606  gonan0  32646  goaln0  32647  gonarlem  32648  gonar  32649  goalrlem  32650  goalr  32651  fmla0disjsuc  32652  fmlasucdisj  32653  satffunlem  32655  satffunlem1lem1  32656  satffunlem2lem1  32658  msubff1  32810  mvhf1  32813  brtp  32992  br8  32999  br6  33000  br4  33001  brsegle  33576  copsex2b  34448  poimirlem4  34939  poimirlem9  34944  dib1dim  38339  diclspsn  38368  dihopelvalcpre  38422  dihmeetlem4preN  38480  dihmeetlem13N  38493  dih1dimatlem  38503  dihatlat  38508  pellexlem3  39567  pellex  39571  snhesn  40267  opelopab4  41040  ichnreuop  43780  ichreuopeq  43781  rrx2xpref1o  44892
  Copyright terms: Public domain W3C validator