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

Theorem preq12d 3748
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 3742 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  { A ,  C }  =  { B ,  D } )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  { A ,  C }  =  { B ,  D } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633   {cpr 3675
This theorem is referenced by:  opeq1  3833  f1oprswap  5553  wunex2  8405  wuncval2  8414  prdsval  13404  imasval  13463  ipoval  14306  frmdval  14522  tmsval  18079  tmsxpsval  18136  uniiccdif  18986  dchrval  20526  disjdifprg  23160  tusval  23462  kur14lem1  24021  kur14  24031  iseupa  24165  eupaseg  24172  eupares  24183  eupap1  24184  eupath2lem3  24187  dfac21  26312  mendval  26639  s4prop  27298  iswlk  27439  istrl  27449  wlkntrllem4  27464  constr1trl  27484  constr2trl  27494  2pthonlem2  27496  redwlk  27502  wlkdvspthlem  27503  eupatrl  27523  usgrcyclnl2  27525  3v3e3cycl1  27528  constr3trllem5  27538  4cycl4v4e  27550  4cycl4dv4e  27552  frgra2v  27591  frgra3vlem1  27592  frgra3vlem2  27593  4cycl2vnunb  27609  tgrpfset  30751  tgrpset  30752  hlhilset  31945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-un 3191  df-sn 3680  df-pr 3681
  Copyright terms: Public domain W3C validator