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

Theorem preq12d 4102
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 4096 . 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 1383   {cpr 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017
This theorem is referenced by:  opeq1  4202  f1oprswap  5845  wunex2  9119  wuncval2  9128  s4prop  12845  wrdlen2  12868  wwlktovf  12876  wwlktovf1  12877  wwlktovfo  12878  wrd2f1tovbij  12880  prdsval  14834  ipoval  15763  frmdval  15998  symg2bas  16402  tusval  20747  tmsval  20962  tmsxpsval  21019  uniiccdif  21965  dchrval  23487  eengv  24260  iswlk  24498  wlkelwrd  24508  istrl  24517  wlkntrllem2  24540  2wlklem  24544  constr1trl  24568  2pthlem2  24576  2wlklem1  24577  redwlk  24586  wlkdvspthlem  24587  3v3e3cycl1  24622  constr3trllem5  24632  4cycl4v4e  24644  4cycl4dv4e  24646  iswwlk  24661  wlkiswwlk2lem2  24670  wlkiswwlk2lem5  24673  wwlknred  24701  wwlknext  24702  wwlknredwwlkn  24704  wwlkm1edg  24713  wwlkextproplem2  24720  isclwwlk  24746  clwwlkprop  24748  clwwlkgt0  24749  clwwlkn2  24753  clwlkisclwwlklem2a1  24757  clwlkisclwwlklem2fv1  24760  clwlkisclwwlklem2a4  24762  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  clwlkisclwwlk  24767  clwwlkel  24771  clwwlkf  24772  clwwlkext2edg  24780  wwlkext2clwwlk  24781  wwlksubclwwlk  24782  clwwisshclwwlem1  24783  clwwisshclwwlem  24784  clwwisshclww  24785  usg2cwwk2dif  24798  clwlkfclwwlk  24822  rusgrasn  24923  rusgranumwlkl1  24925  iseupa  24943  eupatrl  24946  eupaseg  24951  eupares  24953  eupap1  24954  eupath2lem3  24957  frgra2v  24977  frgra3vlem1  24978  frgra3vlem2  24979  4cycl2vnunb  24995  extwwlkfablem1  25052  extwwlkfablem2  25056  numclwwlkovf2ex  25064  disjdifprg  27414  kur14lem1  28628  kur14  28638  dfac21  30988  mendval  31108  usgra2pthlem1  32307  usgra2pth  32308  usgra2adedglem1  32310  zlmodzxzsub  32817  tgrpfset  36345  tgrpset  36346  hlhilset  37539
  Copyright terms: Public domain W3C validator