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

Theorem sbequ 1999
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 1998 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 1998 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1652 . 2  |-  ( x  =  y  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
41, 3impbid 185 1  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   [wsb 1631
This theorem is referenced by:  drsb2  2000  sbco2  2025  sb10f  2064  sb8eu  2162  cbvab  2402  cbvralf  2759  cbvreu  2763  cbvralsv  2776  cbvrexsv  2777  cbvrab  2787  cbvreucsf  3146  cbvrabcsf  3147  sbss  3564  cbvopab1  4090  cbvmpt  4111  tfis  4644  tfisi  4648  tfinds  4649  findes  4685  cbviota  6257  sb8iota  6259  cbvriota  6310  uzind4s  10273
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632
  Copyright terms: Public domain W3C validator