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

Theorem sbequ 2101
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 2100 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2100 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1779 . 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 1724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-13 1983
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-nf 1602  df-sb 1725
This theorem is referenced by:  drsb2  2103  sbcom3  2137  sbco2  2142  sbcom2  2173  sb10f  2184  sb8eu  2302  sb8euOLD  2303  cbvabOLD  2583  cbvralf  3062  cbvreu  3066  cbvralsv  3079  cbvrexsv  3080  cbvrab  3091  cbvreucsf  3451  cbvrabcsf  3452  sbss  3920  cbvopab1  4503  cbvmpt  4523  cbviota  5542  sb8iota  5544  cbvriota  6248  tfis  6670  tfinds  6675  findes  6711  uzind4s  11145  wl-sbcom2d-lem1  29977  wl-sb8eut  29990  wl-sbcom3  30003  sbeqi  30536
  Copyright terms: Public domain W3C validator