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

Theorem preq12d 4467
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 4461 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 575 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {cpr 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-un 3774  df-sn 4371  df-pr 4373
This theorem is referenced by:  opeq1  4595  csbopg  4613  opthhausdorff  5172  opthhausdorff0  5173  f1oprswap  6392  wunex2  9841  wuncval2  9850  s4prop  13875  wrdlen2  13909  wwlktovf  13920  wwlktovf1  13921  wwlktovfo  13922  wrd2f1tovbij  13924  prdsval  16316  ipoval  17355  frmdval  17589  symg2bas  18015  tusval  22280  tmsval  22496  tmsxpsval  22553  uniiccdif  23558  dchrval  25172  eengv  26072  wkslem1  26730  wkslem2  26731  iswlk  26733  wlkonl1iedg  26788  2wlklem  26790  redwlk  26796  wlkp1lem7  26803  wlkp1lem8  26804  wlkdlem2  26807  upgrwlkdvdelem  26859  usgr2pthlem  26886  usgr2pth  26887  crctcshwlkn0lem4  26933  crctcshwlkn0lem5  26934  crctcshwlkn0lem6  26935  iswwlks  26956  0enwwlksnge1  26990  wlkiswwlks2lem2  26996  wlkiswwlks2lem5  26999  wwlksm1edg  27007  wwlksnred  27028  wwlksnext  27029  wwlksnredwwlkn  27031  wwlksnextproplem2  27047  2wlkdlem10  27074  umgrwwlks2on  27097  rusgrnumwwlkl1  27109  isclwwlk  27126  clwwlkccatlem  27131  clwwlkccat  27132  clwlkclwwlklem2a1  27134  clwlkclwwlklem2fv1  27137  clwlkclwwlklem2a4  27139  clwlkclwwlklem2a  27140  clwlkclwwlklem2  27142  clwlkclwwlk  27144  clwwisshclwwslemlem  27155  clwwisshclwwslem  27156  clwwisshclwws  27157  clwwlkinwwlk  27188  clwwlkn2  27192  clwwlkel  27194  clwwlkf  27195  clwwlkwwlksb  27203  clwwlkext2edg  27205  wwlksext2clwwlk  27206  wwlksext2clwwlkOLD  27207  wwlksubclwwlk  27208  umgr2cwwk2dif  27214  clwlksfclwwlkOLD  27235  s2elclwwlknon2  27271  clwwlknonex2lem2  27276  clwwlknonex2  27277  3wlkdlem10  27341  upgr3v3e3cycl  27352  upgr4cycl4dv4e  27357  eupthseg  27378  upgreupthseg  27381  eupth2lem3  27408  nfrgr2v  27446  frgr3vlem1  27447  frgr3vlem2  27448  4cycl2vnunb  27464  extwwlkfablem1OLD  27516  disjdifprg  29712  kur14lem1  31509  kur14  31519  tgrpfset  36522  tgrpset  36523  hlhilset  37712  dfac21  38134  mendval  38251  sge0sn  41072  isupwlk  42282  zlmodzxzsub  42703  onsetreclem1  43016
  Copyright terms: Public domain W3C validator