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

Theorem preq12d 3962
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 3956 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  { A ,  C }  =  { B ,  D } )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  { A ,  C }  =  { B ,  D } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   {cpr 3879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-sn 3878  df-pr 3880
This theorem is referenced by:  opeq1  4059  f1oprswap  5680  wunex2  8905  wuncval2  8914  s4prop  12525  wrdlen2  12548  prdsval  14393  ipoval  15324  frmdval  15529  symg2bas  15903  tusval  19841  tmsval  20056  tmsxpsval  20113  uniiccdif  21058  dchrval  22573  eengv  23225  iswlk  23426  istrl  23436  wlkntrllem2  23459  2wlklem  23463  constr1trl  23487  2pthlem2  23495  2wlklem1  23496  redwlk  23505  wlkdvspthlem  23506  usgrcyclnl2  23527  3v3e3cycl1  23530  constr3trllem5  23540  4cycl4v4e  23552  4cycl4dv4e  23554  iseupa  23586  eupatrl  23589  eupaseg  23594  eupares  23596  eupap1  23597  eupath2lem3  23600  disjdifprg  25919  kur14lem1  27094  kur14  27104  dfac21  29419  mendval  29540  wwlktovf  30251  wwlktovf1  30252  wwlktovfo  30253  wrd2f1tovbij  30255  wlkelwrd  30280  usgra2pthspth  30295  usgra2wlkspthlem1  30296  usgra2pthlem1  30300  usgra2pth  30301  usgra2adedglem1  30308  iswwlk  30317  wlkiswwlk2lem2  30326  wlkiswwlk2lem5  30329  wwlknred  30355  wwlknext  30356  wwlknredwwlkn  30358  wwlkm1edg  30367  isclwwlk  30431  clwwlkprop  30433  clwwlkgt0  30434  clwwlkn2  30438  clwlkisclwwlklem2a1  30441  clwlkisclwwlklem2fv1  30444  clwlkisclwwlklem2a4  30446  clwlkisclwwlklem2a  30447  clwlkisclwwlklem1  30449  clwlkisclwwlk  30451  clwwlkel  30455  clwwlkf  30456  clwwlkext2edg  30464  wwlkext2clwwlk  30465  wwlksubclwwlk  30466  clwwisshclwwlem1  30469  clwwisshclwwlem  30470  clwwisshclww  30471  usg2cwwk2dif  30494  clwlkfclwwlk  30517  rusgrasn  30557  rusgranumwlkl1  30559  wwlkextproplem2  30561  frgra2v  30591  frgra3vlem1  30592  frgra3vlem2  30593  4cycl2vnunb  30609  extwwlkfablem1  30667  extwwlkfablem2  30671  numclwwlkovf2ex  30679  zlmodzxzsub  30757  tgrpfset  34388  tgrpset  34389  hlhilset  35582
  Copyright terms: Public domain W3C validator