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

Theorem preq12d 4114
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 4108 . 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 1379   {cpr 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030
This theorem is referenced by:  opeq1  4213  f1oprswap  5854  wunex2  9115  wuncval2  9124  s4prop  12825  wrdlen2  12848  wwlktovf  12856  wwlktovf1  12857  wwlktovfo  12858  wrd2f1tovbij  12860  prdsval  14709  ipoval  15640  frmdval  15848  symg2bas  16225  tusval  20520  tmsval  20735  tmsxpsval  20792  uniiccdif  21738  dchrval  23253  eengv  23974  iswlk  24212  wlkelwrd  24222  istrl  24231  wlkntrllem2  24254  2wlklem  24258  constr1trl  24282  2pthlem2  24290  2wlklem1  24291  redwlk  24300  wlkdvspthlem  24301  usgra2wlkspthlem1  24311  usgrcyclnl2  24333  3v3e3cycl1  24336  constr3trllem5  24346  4cycl4v4e  24358  4cycl4dv4e  24360  iswwlk  24375  wlkiswwlk2lem2  24384  wlkiswwlk2lem5  24387  wwlknred  24415  wwlknext  24416  wwlknredwwlkn  24418  wwlkm1edg  24427  wwlkextproplem2  24434  isclwwlk  24460  clwwlkprop  24462  clwwlkgt0  24463  clwwlkn2  24467  clwlkisclwwlklem2a1  24471  clwlkisclwwlklem2fv1  24474  clwlkisclwwlklem2a4  24476  clwlkisclwwlklem2a  24477  clwlkisclwwlklem1  24479  clwlkisclwwlk  24481  clwwlkel  24485  clwwlkf  24486  clwwlkext2edg  24494  wwlkext2clwwlk  24495  wwlksubclwwlk  24496  clwwisshclwwlem1  24497  clwwisshclwwlem  24498  clwwisshclww  24499  usg2cwwk2dif  24512  clwlkfclwwlk  24536  rusgrasn  24637  rusgranumwlkl1  24639  iseupa  24657  eupatrl  24660  eupaseg  24665  eupares  24667  eupap1  24668  eupath2lem3  24671  frgra2v  24691  frgra3vlem1  24692  frgra3vlem2  24693  4cycl2vnunb  24709  extwwlkfablem1  24767  extwwlkfablem2  24771  numclwwlkovf2ex  24779  disjdifprg  27125  kur14lem1  28306  kur14  28316  dfac21  30632  mendval  30753  usgra2pthspth  31834  usgra2pthlem1  31836  usgra2pth  31837  usgra2adedglem1  31839  zlmodzxzsub  32033  tgrpfset  35549  tgrpset  35550  hlhilset  36743
  Copyright terms: Public domain W3C validator