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

Theorem preq1d 4055
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 4049 . 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 1370   {cpr 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-v 3067  df-un 3428  df-sn 3973  df-pr 3975
This theorem is referenced by:  opthwiener  4688  fprg  5987  dfac2  8398  symg2bas  16002  2pthoncl  23634  eupath2lem3  23732  fprb  27715  wopprc  29514  wwlknredwwlkn  30493  clwwlkgt0  30569  clwlkisclwwlklem2fv1  30579  clwlkisclwwlklem2fv2  30580  clwlkisclwwlklem2a  30582  clwlkisclwwlklem0  30585  clwwisshclwwlem  30605  wwlkextprop  30698  frgraunss  30722  frgra1v  30725  frgra2v  30726  frgra3v  30729  n4cyclfrgra  30745
  Copyright terms: Public domain W3C validator