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

Theorem sbequ 2121
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 2120 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2120 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1803 . 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 1747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862  ax-13 2006
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625  df-sb 1748
This theorem is referenced by:  drsb2  2123  sbcom3  2157  sbco2  2162  sbcom2  2193  sb10f  2204  sb8eu  2253  sb8euOLD  2254  cbvabOLD  2524  cbvralf  3003  cbvreu  3007  cbvralsv  3020  cbvrexsv  3021  cbvrab  3032  cbvreucsf  3382  cbvrabcsf  3383  sbss  3855  cbvopab1  4437  cbvmpt  4457  cbviota  5465  sb8iota  5467  cbvriota  6168  tfis  6588  tfinds  6593  findes  6629  uzind4s  11061  wl-sbcom2d-lem1  30174  wl-sb8eut  30187  wl-sbcom3  30200  sbeqi  30734
  Copyright terms: Public domain W3C validator