Theorem sbequ12 1956

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 1955	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1708	. 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 1706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1707

This theorem is referenced by:  sbequ12r  1957  sbequ12a  1958  sbequ12aOLD  1959  axc16ALT  2073  nfsb4t  2098  sbcoOLD  2125  sbco2  2129  sbco2OLD  2130  sb8  2142  sb8e  2143  sbcom2OLD  2169  sb6aOLD  2173  sbal1  2188  sbal1OLD  2189  mopickOLDOLD  2358  2moOLDOLD  2379  2eu6OLD  2389  clelab  2606  clelabOLD  2607  sbab  2609  cbvralf  3077  cbvralsv  3094  cbvrexsv  3095  cbvrab  3106  sbhypf  3155  mob2  3278  reu2  3286  reu6  3287  sbcralt  3407  sbcrexgOLD  3412  sbcreu  3413  sbcreugOLD  3414  cbvreucsf  3464  cbvrabcsf  3465  csbif  3984  csbifgOLD  3985  rabasiun  4324  cbvopab1  4512  cbvopab1s  4514  cbvmpt  4532  opelopabsb  4752  csbopab  4774  csbopabgALT  4775  opeliunxp  5045  ralxpf  5142  cbviota  5549  csbiota  5573  csbiotagOLD  5574  cbvriota  6248  csbriota  6250  onminex  6615  tfis  6662  findes  6703  abrexex2g  6753  opabex3d  6754  opabex3  6755  abrexex2  6757  dfoprab4f  6834  uzind4s  11132  cbvmptf  27154  nn0min  27267  esumcvg  27720  wl-sb8t  29565  wl-sbalnae  29577  wl-ax11-lem8  29597  pm13.193  30853  opeliun2xp  31863  bj-sbab  33328