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

Theorem sbequ 2225
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 2224 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2224 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1872 . 2  |-  ( x  =  y  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
41, 3impbid 195 1  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   [wsb 1805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-13 2104
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806
This theorem is referenced by:  drsb2  2227  sbcom3  2260  sbco2  2264  sbcom2  2294  sb10f  2305  sb8eu  2352  cbvralf  2999  cbvreu  3003  cbvralsv  3016  cbvrexsv  3017  cbvrab  3029  cbvreucsf  3383  cbvrabcsf  3384  sbss  3870  cbvopab1  4466  cbvmpt  4487  cbviota  5558  sb8iota  5560  cbvriota  6280  tfis  6700  tfinds  6705  findes  6742  uzind4s  11242  wl-sbcom2d-lem1  31959  wl-sb8eut  31976  wl-sbcom3  31989  sbeqi  32467  disjinfi  37539
  Copyright terms: Public domain W3C validator