Theorem sbequ12 1935

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

Step	Hyp	Ref	Expression
1		sbequ1 1934	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1701	. 2 |- ( x = y -> ( [ y / x ] ph -> ph ) )
3	1, 2	impbid 191	1 |- ( x = y -> ( ph <-> [ y / x ] ph ) )

Syntax hints:   -> wi 4   <-> wb 184   [wsb 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-sb 1700

This theorem is referenced by:  sbequ12r  1936  sbequ12a  1937  sbequ12aOLD  1938  nfsb4t  2078  axc16ALT  2103  axc16ALT2  2104  sbcoOLD  2108  sbco2  2112  sbco2OLD  2113  sbcomOLD  2118  sb8  2126  sb8e  2127  sbcom2OLD  2154  sb6aOLD  2158  sbal1  2173  sbal1OLD  2174  mopickOLD  2337  2mo  2355  2moOLD  2356  2eu6  2363  clelab  2553  sbab  2555  cbvralf  2931  cbvralsv  2948  cbvrexsv  2949  cbvrab  2960  sbhypf  3008  mob2  3128  reu2  3136  reu6  3137  sbcralt  3255  sbcrexgOLD  3260  sbcreu  3261  sbcreugOLD  3262  cbvreucsf  3309  cbvrabcsf  3310  csbif  3827  csbifgOLD  3828  cbvopab1  4350  cbvopab1s  4352  cbvmpt  4370  opelopabsb  4588  csbopab  4609  csbopabgOLD  4610  opeliunxp  4877  ralxpf  4973  cbviota  5374  csbiota  5398  csbiotagOLD  5399  cbvriota  6050  csbriota  6052  onminex  6407  tfis  6454  findes  6495  abrexex2g  6543  opabex3d  6544  opabex3  6545  abrexex2  6547  dfoprab4f  6621  uzind4s  10901  cbvmptf  25794  nn0min  25912  esumcvg  26388  wl-sb8t  28222  wl-sbalnae  28234  wl-ax11-lem8  28249  pm13.193  29507  rabasiun  30073  opeliun2xp  30562  bj-sbab  31924