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

Theorem sbequ 1952
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 1951 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 1951 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1825 . 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 1882
This theorem is referenced by:  drsb2  1953  sbco2  1980  sb10f  2082  sb8eu  2132  cbvab  2367  cbvralf  2703  cbvreu  2707  cbvralsv  2714  cbvrexsv  2715  cbvrab  2725  cbvreucsf  3073  cbvrabcsf  3074  sbss  3469  cbvopab1  3986  cbvmpt  4007  tfis  4536  tfisi  4540  tfinds  4541  findes  4577  cbviota  6148  sb8iota  6150  cbvriota  6201  uzind4s  10157
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883
  Copyright terms: Public domain W3C validator