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

Theorem sbequ 2013
Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 2012 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2012 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1666 . 2  |-  ( x  =  y  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
41, 3impbid 183 1  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   [wsb 1638
This theorem is referenced by:  drsb2  2014  sbco2  2039  sb10f  2074  sb8eu  2174  cbvab  2414  cbvralf  2771  cbvreu  2775  cbvralsv  2788  cbvrexsv  2789  cbvrab  2799  cbvreucsf  3158  cbvrabcsf  3159  sbss  3576  cbvopab1  4105  cbvmpt  4126  tfis  4661  tfisi  4665  tfinds  4666  findes  4702  cbviota  5240  sb8iota  5242  cbvriota  6331  uzind4s  10294  cbvmptf  23235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639
  Copyright terms: Public domain W3C validator