Theorem sbequ12 1936

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 1935	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1702	. 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 1700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701

This theorem is referenced by:  sbequ12r  1937  sbequ12a  1938  sbequ12aOLD  1939  axc16ALT  2055  nfsb4t  2080  sbcoOLD  2107  sbco2  2111  sbco2OLD  2112  sb8  2124  sb8e  2125  sbcom2OLD  2152  sb6aOLD  2156  sbal1  2171  sbal1OLD  2172  mopickOLDOLD  2341  2moOLDOLD  2362  2eu6OLD  2372  clelab  2571  clelabOLD  2572  sbab  2574  cbvralf  2962  cbvralsv  2979  cbvrexsv  2980  cbvrab  2991  sbhypf  3040  mob2  3160  reu2  3168  reu6  3169  sbcralt  3288  sbcrexgOLD  3293  sbcreu  3294  sbcreugOLD  3295  cbvreucsf  3342  cbvrabcsf  3343  csbif  3860  csbifgOLD  3861  cbvopab1  4383  cbvopab1s  4385  cbvmpt  4403  opelopabsb  4620  csbopab  4641  csbopabgALT  4642  opeliunxp  4911  ralxpf  5007  cbviota  5407  csbiota  5431  csbiotagOLD  5432  cbvriota  6083  csbriota  6085  onminex  6439  tfis  6486  findes  6527  abrexex2g  6575  opabex3d  6576  opabex3  6577  abrexex2  6579  dfoprab4f  6653  uzind4s  10935  cbvmptf  25993  nn0min  26112  esumcvg  26557  wl-sb8t  28402  wl-sbalnae  28414  wl-ax11-lem8  28434  pm13.193  29691  rabasiun  30256  opeliun2xp  30746  bj-sbab  32401