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

Theorem sbequ 2090
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 2089 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2089 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1744 . 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 1711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712
This theorem is referenced by:  drsb2  2092  sbcom3  2128  sbco2  2134  sbco2OLD  2135  sbcom2  2173  sb10f  2188  sb8eu  2314  sb8euOLD  2315  sb8euOLDOLD  2316  cbvabOLD  2609  cbvralf  3082  cbvreu  3086  cbvralsv  3099  cbvrexsv  3100  cbvrab  3111  cbvreucsf  3469  cbvrabcsf  3470  sbss  3937  cbvopab1  4517  cbvmpt  4537  cbviota  5554  sb8iota  5556  cbvriota  6253  tfis  6667  tfinds  6672  findes  6708  uzind4s  11137  wl-sbcom2d-lem1  29586  wl-sb8eut  29599  wl-sbcom3  29612  sbeqi  30172  frege52b  36883
  Copyright terms: Public domain W3C validator