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

Theorem preq12d 4251
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypotheses
Ref Expression
preq1d.1 (𝜑𝐴 = 𝐵)
preq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
preq12d (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Proof of Theorem preq12d
StepHypRef Expression
1 preq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 preq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 preq12 4245 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 692 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {cpr 4155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-sn 4154  df-pr 4156
This theorem is referenced by:  opeq1  4375  csbopg  4393  f1oprswap  6139  wunex2  9505  wuncval2  9514  s4prop  13586  wrdlen2  13617  wwlktovf  13628  wwlktovf1  13629  wwlktovfo  13630  wrd2f1tovbij  13632  prdsval  16031  ipoval  17070  frmdval  17304  symg2bas  17734  tusval  21975  tmsval  22191  tmsxpsval  22248  uniiccdif  23247  dchrval  24854  eengv  25754  wkslem1  26367  wkslem2  26368  iswlk  26370  wlkonl1iedg  26424  2wlklem  26426  redwlk  26432  wlkp1lem7  26439  wlkp1lem8  26440  wlkdlem2  26443  upgrwlkdvdelem  26495  usgr2pthlem  26522  usgr2pth  26523  crctcshwlkn0lem4  26568  crctcshwlkn0lem5  26569  crctcshwlkn0lem6  26570  iswwlks  26591  0enwwlksnge1  26612  wlkiswwlks2lem2  26619  wlkiswwlks2lem5  26622  wwlksm1edg  26630  wwlksnred  26650  wwlksnext  26651  wwlksnredwwlkn  26653  wwlksnextproplem2  26668  2wlkdlem10  26694  umgrwwlks2on  26713  rusgrnumwwlkl1  26724  isclwwlks  26741  clwlkclwwlklem2a1  26754  clwlkclwwlklem2fv1  26757  clwlkclwwlklem2a4  26759  clwlkclwwlklem2a  26760  clwlkclwwlklem2  26762  clwlkclwwlk  26764  clwwlksn2  26770  clwwlksel  26774  clwwlksf  26775  clwwlksext2edg  26783  wwlksext2clwwlk  26784  wwlksubclwwlks  26785  clwwisshclwwslemlem  26786  clwwisshclwwslem  26787  clwwisshclwws  26788  umgr2cwwk2dif  26801  clwlksfclwwlk  26822  3wlkdlem10  26889  upgr3v3e3cycl  26900  upgr4cycl4dv4e  26905  eupthseg  26926  upgreupthseg  26929  eupth2lem3  26956  nfrgr2v  26994  frgr3vlem1  26995  frgr3vlem2  26996  4cycl2vnunb  27012  extwwlkfablem1  27060  extwwlkfablem2  27062  numclwwlkovf2ex  27069  disjdifprg  29224  kur14lem1  30888  kur14  30898  tgrpfset  35498  tgrpset  35499  hlhilset  36692  dfac21  37102  mendval  37220  sge0sn  39890  isupwlk  40993  zlmodzxzsub  41399  onsetreclem1  41715
  Copyright terms: Public domain W3C validator