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

Theorem preq12 4670
 Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Assertion
Ref Expression
preq12 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Proof of Theorem preq12
StepHypRef Expression
1 preq1 4668 . 2 (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2 preq2 4669 . 2 (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
31, 2sylan9eq 2881 1 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1530  {cpr 4566 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-sn 4565  df-pr 4567 This theorem is referenced by:  preq12i  4673  preq12d  4676  ssprsseq  4757  preq12b  4780  prnebg  4785  preq12nebg  4792  opthprneg  4794  snex  5328  relop  5720  opthreg  9070  hashle2pr  13825  wwlktovfo  14312  joinval  17605  meetval  17619  ipole  17758  sylow1  18648  frgpuplem  18818  uspgr2wlkeq  27341  wlkres  27366  wlkp1lem8  27376  usgr2pthlem  27458  2wlkdlem10  27628  1wlkdlem4  27833  3wlkdlem6  27858  3wlkdlem10  27862  pfxwlk  32254  oppr  43131  imarnf1pr  43347  elsprel  43469  sprsymrelf1lem  43485  sprsymrelf  43489  paireqne  43505  sbcpr  43515  isomuspgrlem2b  43826  isomuspgrlem2d  43828
 Copyright terms: Public domain W3C validator