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

Theorem sbequ 2171
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 2170 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2170 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1846 . 2  |-  ( x  =  y  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
41, 3impbid 194 1  |-  ( x  =  y  ->  ( [ x  /  z ] ph  <->  [ y  /  z ] ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   [wsb 1787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-12 1906  ax-13 2054
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788
This theorem is referenced by:  drsb2  2173  sbcom3  2206  sbco2  2210  sbcom2  2241  sb10f  2252  sb8eu  2300  cbvabOLD  2565  cbvralf  3050  cbvreu  3054  cbvralsv  3067  cbvrexsv  3068  cbvrab  3080  cbvreucsf  3431  cbvrabcsf  3432  sbss  3909  cbvopab1  4493  cbvmpt  4514  cbviota  5569  sb8iota  5571  cbvriota  6276  tfis  6694  tfinds  6699  findes  6736  uzind4s  11225  wl-sbcom2d-lem1  31851  wl-sb8eut  31868  wl-sbcom3  31887  sbeqi  32365  disjinfi  37366
  Copyright terms: Public domain W3C validator