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

Theorem sbequ12 1944
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 1943 . 2  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
2 sbequ2 1660 . 2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
31, 2impbid 184 1  |-  ( x  =  y  ->  ( ph 
<->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   [wsb 1658
This theorem is referenced by:  sbequ12r  1945  sbequ12a  1946  sbid  1947  nfsb4t  2127  nfsb4tOLD  2128  ax16ALT  2154  ax16ALT2  2155  sbco  2158  sbco2  2161  sbcom  2164  sbcomOLD  2165  sb8  2168  sb8e  2169  sbcom2  2190  sb6a  2193  sbal1  2203  mopick  2343  2mo  2359  2eu6  2366  clelab  2556  sbab  2558  cbvralf  2926  cbvralsv  2943  cbvrexsv  2944  cbvrab  2954  sbhypf  3001  mob2  3114  reu2  3122  reu6  3123  sbcralt  3233  sbcralg  3235  sbcrexg  3236  sbcreug  3237  cbvreucsf  3313  cbvrabcsf  3314  csbifg  3767  cbvopab1  4278  cbvopab1s  4280  csbopabg  4283  cbvmpt  4299  opelopabsb  4465  onminex  4787  tfis  4834  findes  4875  opeliunxp  4929  ralxpf  5019  cbviota  5423  csbiotag  5447  abrexex2g  5988  opabex3d  5989  opabex3  5990  abrexex2  6001  dfoprab4f  6405  cbvriota  6560  csbriotag  6562  uzind4s  10536  cbvmptf  24068  esumcvg  24476  pm13.193  27588  nfsb4twAUX7  29576  sbcoNEW7  29582  sbco2wAUX7  29585  sbcomwAUX7  29588  sb6aNEW7  29611  sbal1NEW7  29615  ax16ALTNEW7  29635  sbcom2NEW7  29644  ax16ALT2OLD7  29743  nfsb4tOLD7  29745  nfsb4tw2AUXOLD7  29746  sbco2OLD7  29752  sbcomOLD7  29755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659
  Copyright terms: Public domain W3C validator