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

Theorem sbequ 2077
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 2076 . 2  |-  ( x  =  y  ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph ) )
2 sbequi 2076 . . 3  |-  ( y  =  x  ->  ( [ y  /  z ] ph  ->  [ x  /  z ] ph ) )
32equcoms 1735 . 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 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703
This theorem is referenced by:  drsb2  2079  sbcom3  2115  sbco2  2121  sbco2OLD  2122  sbcom2  2160  sb10f  2175  sb8eu  2301  sb8euOLD  2302  sb8euOLDOLD  2303  cbvabOLD  2596  cbvralf  3045  cbvreu  3049  cbvralsv  3062  cbvrexsv  3063  cbvrab  3074  cbvreucsf  3428  cbvrabcsf  3429  sbss  3896  cbvopab1  4469  cbvmpt  4489  cbviota  5493  sb8iota  5495  cbvriota  6170  tfis  6574  tfinds  6579  findes  6615  uzind4s  11024  wl-sbcom2d-lem1  28532  wl-sb8eut  28545  wl-sbcom3  28558  sbeqi  29119
  Copyright terms: Public domain W3C validator