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

Theorem sbequ 2067
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, 14-May-1993.)
Assertion
Ref Expression
sbequ  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 2066 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2066 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1733 . 2  |-  ( x  =  y  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
41, 3impbid 191 1  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   [wsb 1700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701
This theorem is referenced by:  drsb2  2069  sbcom3  2105  sbco2  2111  sbco2OLD  2112  sbcom2  2151  sb10f  2166  sb8eu  2290  sb8euOLD  2291  sb8euOLDOLD  2292  cbvab  2556  cbvralf  2936  cbvreu  2940  cbvralsv  2953  cbvrexsv  2954  cbvrab  2965  cbvreucsf  3316  cbvrabcsf  3317  sbss  3784  cbvopab1  4357  cbvmpt  4377  cbviota  5381  sb8iota  5383  cbvriota  6057  tfis  6460  tfinds  6465  findes  6501  uzind4s  10906  wl-sbcom2d-lem1  28336  wl-sb8eut  28351  wl-sbcom3  28364  sbeqi  28925
  Copyright terms: Public domain W3C validator