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

Theorem preq12d 4700
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 4694 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 584 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  {cpr 4586
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-un 3913  df-sn 4585  df-pr 4587
This theorem is referenced by:  opeq1  4828  csbopg  4846  opthhausdorff  5472  opthhausdorff0  5473  f1oprswap  6825  wunex2  10670  wuncval2  10679  s4prop  14791  wrdlen2  14825  wwlktovf  14837  wwlktovf1  14838  wwlktovfo  14839  wrd2f1tovbij  14841  prdsval  17329  xpsfval  17440  xpsval  17444  ipoval  18411  frmdval  18653  symg2bas  19165  xpstopnlem2  23146  tusval  23601  tmsval  23820  tmsxpsval  23878  uniiccdif  24926  dchrval  26566  eengv  27814  wkslem1  28441  wkslem2  28442  iswlk  28444  wlkonl1iedg  28499  2wlklem  28501  redwlk  28506  wlkp1lem7  28513  wlkdlem2  28517  upgrwlkdvdelem  28570  usgr2pthlem  28597  usgr2pth  28598  crctcshwlkn0lem4  28644  crctcshwlkn0lem5  28645  crctcshwlkn0lem6  28646  iswwlks  28667  0enwwlksnge1  28695  wlkiswwlks2lem2  28701  wlkiswwlks2lem5  28704  wwlksm1edg  28712  wwlksnred  28723  wwlksnext  28724  wwlksnredwwlkn  28726  wwlksnextproplem2  28741  2wlkdlem10  28766  umgrwwlks2on  28788  rusgrnumwwlkl1  28799  isclwwlk  28814  clwwlkccatlem  28819  clwwlkccat  28820  clwlkclwwlklem2a1  28822  clwlkclwwlklem2fv1  28825  clwlkclwwlklem2a4  28827  clwlkclwwlklem2a  28828  clwlkclwwlklem2  28830  clwlkclwwlk  28832  clwwisshclwwslemlem  28843  clwwisshclwwslem  28844  clwwisshclwws  28845  clwwlkinwwlk  28870  clwwlkn2  28874  clwwlkel  28876  clwwlkf  28877  clwwlkwwlksb  28884  clwwlkext2edg  28886  wwlksext2clwwlk  28887  wwlksubclwwlk  28888  umgr2cwwk2dif  28894  s2elclwwlknon2  28934  clwwlknonex2lem2  28938  clwwlknonex2  28939  3wlkdlem10  28999  upgr3v3e3cycl  29010  upgr4cycl4dv4e  29015  eupthseg  29036  upgreupthseg  29039  eupth2lem3  29066  nfrgr2v  29102  frgr3vlem1  29103  frgr3vlem2  29104  4cycl2vnunb  29120  disjdifprg  31379  s2rn  31683  idlsrgval  32124  revwlk  33587  kur14lem1  33669  kur14  33679  bj-endval  35753  tgrpfset  39174  tgrpset  39175  hlhilset  40364  dfac21  41331  mendval  41448  mnurndlem1  42503  sge0sn  44552  isomuspgrlem2b  45953  isupwlk  45970  zlmodzxzsub  46368  2arymaptf  46670  prelrrx2b  46732  rrx2plordisom  46741  onsetreclem1  47082
  Copyright terms: Public domain W3C validator