Theorem sbequ12 2098

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )

Proof of Theorem sbequ12

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

Syntax hints:   -> wi 4   <-> wb 189   [wsb 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-sb 1806

This theorem is referenced by:  sbequ12r  2099  sbequ12a  2100  axc16ALT  2215  nfsb4t  2238  sbco2  2264  sb8  2273  sb8e  2274  sbal1  2309  clelab  2596  sbab  2598  cbvralf  2999  cbvralsv  3016  cbvrexsv  3017  cbvrab  3029  sbhypf  3081  mob2  3206  reu2  3214  reu6  3215  sbcralt  3328  sbcreu  3332  cbvreucsf  3383  cbvrabcsf  3384  csbif  3922  rabasiun  4273  cbvopab1  4466  cbvopab1s  4468  cbvmptf  4486  cbvmpt  4487  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  opeliunxp  4891  ralxpf  4986  cbviota  5558  csbiota  5582  cbvriota  6280  csbriota  6282  onminex  6653  tfis  6700  findes  6742  abrexex2g  6789  opabex3d  6790  opabex3  6791  abrexex2  6793  dfoprab4f  6870  uzind4s  11242  ac6sf2  28302  esumcvg  28981  bj-sbab  31465  wl-sb8t  31950  wl-sbalnae  31962  wl-ax11-lem8  31986  sbcrexgOLD  35699  pm13.193  36832  opeliun2xp  40622