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

Theorem preq12d 4044
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 4038 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  { A ,  C }  =  { B ,  D } )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  { A ,  C }  =  { B ,  D } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   {cpr 3959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-v 3049  df-un 3407  df-sn 3958  df-pr 3960
This theorem is referenced by:  opeq1  4144  f1oprswap  5776  wunex2  9045  wuncval2  9054  s4prop  12793  wrdlen2  12816  wwlktovf  12824  wwlktovf1  12825  wwlktovfo  12826  wrd2f1tovbij  12828  prdsval  14881  ipoval  15920  frmdval  16155  symg2bas  16559  tusval  20873  tmsval  21088  tmsxpsval  21145  uniiccdif  22091  dchrval  23645  eengv  24424  iswlk  24662  wlkelwrd  24672  istrl  24681  wlkntrllem2  24704  2wlklem  24708  constr1trl  24732  2pthlem2  24740  2wlklem1  24741  redwlk  24750  wlkdvspthlem  24751  3v3e3cycl1  24786  constr3trllem5  24796  4cycl4v4e  24808  4cycl4dv4e  24810  iswwlk  24825  wlkiswwlk2lem2  24834  wlkiswwlk2lem5  24837  wwlknred  24865  wwlknext  24866  wwlknredwwlkn  24868  wwlkm1edg  24877  wwlkextproplem2  24884  isclwwlk  24910  clwwlkprop  24912  clwwlkgt0  24913  clwwlkn2  24917  clwlkisclwwlklem2a1  24921  clwlkisclwwlklem2fv1  24924  clwlkisclwwlklem2a4  24926  clwlkisclwwlklem2a  24927  clwlkisclwwlklem1  24929  clwlkisclwwlk  24931  clwwlkel  24935  clwwlkf  24936  clwwlkext2edg  24944  wwlkext2clwwlk  24945  wwlksubclwwlk  24946  clwwisshclwwlem1  24947  clwwisshclwwlem  24948  clwwisshclww  24949  usg2cwwk2dif  24962  clwlkfclwwlk  24986  rusgrasn  25087  rusgranumwlkl1  25089  iseupa  25107  eupatrl  25110  eupaseg  25115  eupares  25117  eupap1  25118  eupath2lem3  25121  frgra2v  25141  frgra3vlem1  25142  frgra3vlem2  25143  4cycl2vnunb  25159  extwwlkfablem1  25216  extwwlkfablem2  25220  numclwwlkovf2ex  25228  disjdifprg  27594  kur14lem1  28875  kur14  28885  dfac21  31214  mendval  31336  usgra2pthlem1  32706  usgra2pth  32707  usgra2adedglem1  32709  zlmodzxzsub  33184  tgrpfset  36918  tgrpset  36919  hlhilset  38112
  Copyright terms: Public domain W3C validator