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

Theorem sbequ 2000
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 1999 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 1999 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1651 . 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 1629
This theorem is referenced by:  drsb2  2001  sbco2  2026  sb10f  2061  sb8eu  2161  cbvab  2401  cbvralf  2758  cbvreu  2762  cbvralsv  2775  cbvrexsv  2776  cbvrab  2786  cbvreucsf  3145  cbvrabcsf  3146  sbss  3563  cbvopab1  4089  cbvmpt  4110  tfis  4645  tfisi  4649  tfinds  4650  findes  4686  cbviota  5224  sb8iota  5226  cbvriota  6315  uzind4s  10278  cbvmptf  23220
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
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
  Copyright terms: Public domain W3C validator