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

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

Proof of Theorem preq2d
StepHypRef Expression
1 preq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 preq2 3707 . 2  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
31, 2syl 15 1  |-  ( ph  ->  { C ,  A }  =  { C ,  B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {cpr 3641
This theorem is referenced by:  opeq2  3797  opthwiener  4268  opthreg  7319  indislem  16737  iscon  17139  hmphindis  17488  wilthlem2  20307  eupath2lem3  23314  eupath2  23315  fprb  23540  altopthsn  23906  fprg  24545  repcpwti  24573  cbcpcp  24574  pgapspf2  25465  s2prop  27488  frgra2v  27539  frgra3v  27542  mapdindp4  31286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator