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

Theorem preq12d 4412
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 4406 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
41, 2, 3syl2anc 696 1 (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  {cpr 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712  df-sn 4314  df-pr 4316
This theorem is referenced by:  opeq1  4545  csbopg  4563  opthhausdorff  5119  opthhausdorff0  5120  f1oprswap  6333  wunex2  9744  wuncval2  9753  s4prop  13847  wrdlen2  13881  wwlktovf  13892  wwlktovf1  13893  wwlktovfo  13894  wrd2f1tovbij  13896  prdsval  16309  ipoval  17347  frmdval  17581  symg2bas  18010  tusval  22263  tmsval  22479  tmsxpsval  22536  uniiccdif  23538  dchrval  25150  eengv  26050  wkslem1  26705  wkslem2  26706  iswlk  26708  wlkonl1iedg  26763  2wlklem  26765  redwlk  26771  wlkp1lem7  26778  wlkp1lem8  26779  wlkdlem2  26782  upgrwlkdvdelem  26834  usgr2pthlem  26861  usgr2pth  26862  crctcshwlkn0lem4  26908  crctcshwlkn0lem5  26909  crctcshwlkn0lem6  26910  iswwlks  26931  0enwwlksnge1  26965  wlkiswwlks2lem2  26971  wlkiswwlks2lem5  26974  wwlksm1edg  26982  wwlksnred  27002  wwlksnext  27003  wwlksnredwwlkn  27005  wwlksnextproplem2  27020  2wlkdlem10  27047  umgrwwlks2on  27070  rusgrnumwwlkl1  27082  isclwwlk  27099  clwwlkccatlem  27104  clwwlkccat  27105  clwlkclwwlklem2a1  27107  clwlkclwwlklem2fv1  27110  clwlkclwwlklem2a4  27112  clwlkclwwlklem2a  27113  clwlkclwwlklem2  27115  clwlkclwwlk  27117  clwwisshclwwslemlem  27128  clwwisshclwwslem  27129  clwwisshclwws  27130  clwwlkinwwlk  27161  clwwlkn2  27165  clwwlkel  27167  clwwlkf  27168  clwwlkwwlksb  27176  clwwlkext2edg  27178  wwlksext2clwwlk  27179  wwlksext2clwwlkOLD  27180  wwlksubclwwlk  27181  umgr2cwwk2dif  27187  clwlksfclwwlkOLD  27208  s2elclwwlknon2  27244  clwwlknonex2lem2  27249  clwwlknonex2  27250  3wlkdlem10  27313  upgr3v3e3cycl  27324  upgr4cycl4dv4e  27329  eupthseg  27350  upgreupthseg  27353  eupth2lem3  27380  nfrgr2v  27418  frgr3vlem1  27419  frgr3vlem2  27420  4cycl2vnunb  27436  extwwlkfablem1OLD  27489  disjdifprg  29687  kur14lem1  31487  kur14  31497  tgrpfset  36526  tgrpset  36527  hlhilset  37720  dfac21  38130  mendval  38247  sge0sn  41091  isupwlk  42219  zlmodzxzsub  42640  onsetreclem1  42953
  Copyright terms: Public domain W3C validator