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

Theorem sbequ12 1860
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ12  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1859 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1631 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 183 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   [wsb 1629
This theorem is referenced by:  sbequ12r  1861  sbequ12a  1862  sbid  1863  ax16ALT  1987  ax16ALT2  1988  nfsb4t  2020  sbco  2023  sbco2  2026  sbcom  2029  sbcom2  2053  sb6a  2055  sbal1  2065  mopick  2205  2mo  2221  2eu6  2228  clelab  2403  sbab  2405  cbvralf  2758  cbvralsv  2775  cbvrexsv  2776  cbvrab  2786  sbhypf  2833  mob2  2945  reu2  2953  reu6  2954  sbcralt  3063  sbcralg  3065  sbcrexg  3066  sbcreug  3067  cbvreucsf  3145  cbvrabcsf  3146  csbifg  3593  cbvopab1  4089  cbvopab1s  4091  csbopabg  4094  cbvmpt  4110  opelopabsb  4275  onminex  4598  tfis  4645  findes  4686  opeliunxp  4740  ralxpf  4830  cbviota  5224  csbiotag  5248  abrexex2g  5768  opabex3  5769  abrexex2  5780  dfoprab4f  6178  cbvriota  6315  csbriotag  6317  uzind4s  10278  cbvmptf  23220  esumcvg  23454  pm13.193  27611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630
  Copyright terms: Public domain W3C validator