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

Theorem sbequ 2064
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 2063 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2063 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1732 . 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 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-13 1942
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700
This theorem is referenced by:  drsb2  2066  sbcom3  2106  sbco2  2112  sbco2OLD  2113  sbcom2  2153  sb10f  2168  sb8eu  2289  sb8euOLD  2290  cbvab  2551  cbvralf  2931  cbvreu  2935  cbvralsv  2948  cbvrexsv  2949  cbvrab  2960  cbvreucsf  3309  cbvrabcsf  3310  sbss  3777  cbvopab1  4350  cbvmpt  4370  cbviota  5374  sb8iota  5376  cbvriota  6050  tfis  6454  tfinds  6459  findes  6495  uzind4s  10902  wl-sbcom2d-lem1  28233  wl-sb8eut  28242  wl-sbcom3  28255  sbeqi  28816
  Copyright terms: Public domain W3C validator