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

Theorem preq1d 4118
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypothesis
Ref Expression
preq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
preq1d  |-  ( ph  ->  { A ,  C }  =  { B ,  C } )

Proof of Theorem preq1d
StepHypRef Expression
1 preq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 preq1 4112 . 2  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
31, 2syl 16 1  |-  ( ph  ->  { A ,  C }  =  { B ,  C } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   {cpr 4035
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 3120  df-un 3486  df-sn 4034  df-pr 4036
This theorem is referenced by:  opthwiener  4755  fprg  6081  dfac2  8523  symg2bas  16294  2pthoncl  24437  wwlknredwwlkn  24558  wwlkextprop  24576  clwwlkgt0  24603  clwlkisclwwlklem2fv1  24614  clwlkisclwwlklem2fv2  24615  clwlkisclwwlklem2a  24617  clwlkisclwwlklem0  24620  clwwisshclwwlem  24638  eupath2lem3  24811  frgraunss  24827  frgra1v  24830  frgra2v  24831  frgra3v  24834  n4cyclfrgra  24850  fprb  29137  wopprc  30906
  Copyright terms: Public domain W3C validator