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

Theorem preq12d 4637
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 4631 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 587 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  {cpr 4527
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528
This theorem is referenced by:  opeq1  4763  opeq1OLD  4764  csbopg  4783  opthhausdorff  5372  opthhausdorff0  5373  f1oprswap  6633  wunex2  10149  wuncval2  10158  s4prop  14263  wrdlen2  14297  wwlktovf  14311  wwlktovf1  14312  wwlktovfo  14313  wrd2f1tovbij  14315  prdsval  16720  xpsfval  16831  xpsval  16835  ipoval  17756  frmdval  18008  symg2bas  18513  xpstopnlem2  22416  tusval  22872  tmsval  23088  tmsxpsval  23145  uniiccdif  24182  dchrval  25818  eengv  26773  wkslem1  27397  wkslem2  27398  iswlk  27400  wlkonl1iedg  27455  2wlklem  27457  redwlk  27462  wlkp1lem7  27469  wlkdlem2  27473  upgrwlkdvdelem  27525  usgr2pthlem  27552  usgr2pth  27553  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem6  27601  iswwlks  27622  0enwwlksnge1  27650  wlkiswwlks2lem2  27656  wlkiswwlks2lem5  27659  wwlksm1edg  27667  wwlksnred  27678  wwlksnext  27679  wwlksnredwwlkn  27681  wwlksnextproplem2  27696  2wlkdlem10  27721  umgrwwlks2on  27743  rusgrnumwwlkl1  27754  isclwwlk  27769  clwwlkccatlem  27774  clwwlkccat  27775  clwlkclwwlklem2a1  27777  clwlkclwwlklem2fv1  27780  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlk  27787  clwwisshclwwslemlem  27798  clwwisshclwwslem  27799  clwwisshclwws  27800  clwwlkinwwlk  27825  clwwlkn2  27829  clwwlkel  27831  clwwlkf  27832  clwwlkwwlksb  27839  clwwlkext2edg  27841  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  umgr2cwwk2dif  27849  s2elclwwlknon2  27889  clwwlknonex2lem2  27893  clwwlknonex2  27894  3wlkdlem10  27954  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eupthseg  27991  upgreupthseg  27994  eupth2lem3  28021  nfrgr2v  28057  frgr3vlem1  28058  frgr3vlem2  28059  4cycl2vnunb  28075  disjdifprg  30338  s2rn  30646  idlsrgval  31056  revwlk  32484  kur14lem1  32566  kur14  32576  bj-endval  34729  tgrpfset  38040  tgrpset  38041  hlhilset  39230  dfac21  40008  mendval  40125  mnurndlem1  40987  sge0sn  43016  isomuspgrlem2b  44345  isupwlk  44362  zlmodzxzsub  44760  2arymaptf  45064  prelrrx2b  45126  rrx2plordisom  45135  onsetreclem1  45232
  Copyright terms: Public domain W3C validator