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

Theorem preq12d 4253
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 4247 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 692 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {cpr 4157
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 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
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 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-un 3565  df-sn 4156  df-pr 4158
This theorem is referenced by:  opeq1  4377  csbopg  4395  f1oprswap  6147  wunex2  9520  wuncval2  9529  s4prop  13607  wrdlen2  13638  wwlktovf  13649  wwlktovf1  13650  wwlktovfo  13651  wrd2f1tovbij  13653  prdsval  16055  ipoval  17094  frmdval  17328  symg2bas  17758  tusval  22010  tmsval  22226  tmsxpsval  22283  uniiccdif  23286  dchrval  24893  eengv  25793  wkslem1  26407  wkslem2  26408  iswlk  26410  wlkonl1iedg  26464  2wlklem  26466  redwlk  26472  wlkp1lem7  26479  wlkp1lem8  26480  wlkdlem2  26483  upgrwlkdvdelem  26535  usgr2pthlem  26562  usgr2pth  26563  crctcshwlkn0lem4  26608  crctcshwlkn0lem5  26609  crctcshwlkn0lem6  26610  iswwlks  26631  0enwwlksnge1  26652  wlkiswwlks2lem2  26659  wlkiswwlks2lem5  26662  wwlksm1edg  26670  wwlksnred  26690  wwlksnext  26691  wwlksnredwwlkn  26693  wwlksnextproplem2  26708  2wlkdlem10  26734  umgrwwlks2on  26753  rusgrnumwwlkl1  26764  isclwwlks  26781  clwlkclwwlklem2a1  26794  clwlkclwwlklem2fv1  26797  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  clwlkclwwlklem2  26802  clwlkclwwlk  26804  clwwlksn2  26810  clwwlksel  26814  clwwlksf  26815  clwwlksext2edg  26823  wwlksext2clwwlk  26824  wwlksubclwwlks  26825  clwwisshclwwslemlem  26826  clwwisshclwwslem  26827  clwwisshclwws  26828  umgr2cwwk2dif  26841  clwlksfclwwlk  26862  3wlkdlem10  26929  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  eupthseg  26966  upgreupthseg  26969  eupth2lem3  26996  nfrgr2v  27034  frgr3vlem1  27035  frgr3vlem2  27036  4cycl2vnunb  27052  extwwlkfablem1  27100  extwwlkfablem2  27102  numclwwlkovf2ex  27109  disjdifprg  29274  kur14lem1  30949  kur14  30959  tgrpfset  35551  tgrpset  35552  hlhilset  36745  dfac21  37155  mendval  37273  sge0sn  39933  isupwlk  41035  zlmodzxzsub  41456  onsetreclem1  41771
  Copyright terms: Public domain W3C validator