Theorem sbequ12 2111

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 2110	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1882	. 2 |- ( x = y -> ( [ y / x ] ph -> ph ) )
3	1, 2	impbid 202	1 |- ( x = y -> ( ph <-> [ y / x ] ph ) )

Syntax hints:   -> wi 4   <-> wb 196   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881

This theorem is referenced by:  sbequ12r  2112  sbequ12a  2113  axc16ALT  2366  nfsb4t  2389  sbco2  2415  sb8  2424  sb8e  2425  sbal1  2460  clelab  2748  sbab  2750  cbvralf  3165  cbvralsv  3182  cbvrexsv  3183  cbvrab  3198  sbhypf  3253  mob2  3386  reu2  3394  reu6  3395  sbcralt  3510  sbcreu  3515  cbvreucsf  3567  cbvrabcsf  3568  csbif  4138  cbvopab1  4723  cbvopab1s  4725  cbvmptf  4748  cbvmpt  4749  opelopabsb  4985  csbopab  5008  csbopabgALT  5009  opeliunxp  5170  ralxpf  5268  cbviota  5856  csbiota  5881  cbvriota  6621  csbriota  6623  onminex  7007  tfis  7054  findes  7096  abrexex2g  7144  opabex3d  7145  opabex3  7146  abrexex2OLD  7150  dfoprab4f  7226  uzind4s  11748  ac6sf2  29429  esumcvg  30148  bj-sbab  32784  wl-sb8t  33333  wl-sbalnae  33345  wl-ax11-lem8  33369  sbcrexgOLD  37349  pm13.193  38612  opeliun2xp  42111