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

Theorem preq12d 3893
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypotheses
Ref Expression
preq1d.1  |-  ( ph  ->  A  =  B )
preq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
preq12d  |-  ( ph  ->  { A ,  C }  =  { B ,  D } )

Proof of Theorem preq12d
StepHypRef Expression
1 preq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 preq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 preq12 3887 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  { A ,  C }  =  { B ,  D } )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  { A ,  C }  =  { B ,  D } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   {cpr 3817
This theorem is referenced by:  opeq1  3986  f1oprswap  5720  wunex2  8618  wuncval2  8627  s4prop  11867  prdsval  13683  imasval  13742  ipoval  14585  frmdval  14801  tusval  18301  tmsval  18516  tmsxpsval  18573  uniiccdif  19475  dchrval  21023  iswlk  21532  istrl  21542  wlkntrllem2  21565  2wlklem  21569  constr1trl  21593  2pthlem2  21601  2wlklem1  21602  redwlk  21611  wlkdvspthlem  21612  usgrcyclnl2  21633  3v3e3cycl1  21636  constr3trllem5  21646  4cycl4v4e  21658  4cycl4dv4e  21660  iseupa  21692  eupatrl  21695  eupaseg  21700  eupares  21702  eupap1  21703  eupath2lem3  21706  disjdifprg  24022  kur14lem1  24897  kur14  24907  dfac21  27155  mendval  27482  wlkelwrd  28333  usgra2pthspth  28343  usgra2wlkspthlem1  28344  usgra2pthlem1  28348  usgra2pth  28349  usgra2adedglem1  28356  iswwlk  28365  wlkiswwlk2lem2  28374  wlkiswwlk2lem5  28377  frgra2v  28463  frgra3vlem1  28464  frgra3vlem2  28465  4cycl2vnunb  28481  tgrpfset  31615  tgrpset  31616  hlhilset  32809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator