Theorem sbequ12 2083

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

Syntax hints:   -> wi 4   <-> wb 188   [wsb 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-sb 1798

This theorem is referenced by:  sbequ12r  2084  sbequ12a  2085  axc16ALT  2195  nfsb4t  2218  sbco2  2244  sb8  2253  sb8e  2254  sbal1  2289  clelab  2576  sbab  2578  cbvralf  3013  cbvralsv  3030  cbvrexsv  3031  cbvrab  3043  sbhypf  3095  mob2  3218  reu2  3226  reu6  3227  sbcralt  3340  sbcreu  3344  cbvreucsf  3397  cbvrabcsf  3398  csbif  3931  rabasiun  4282  cbvopab1  4473  cbvopab1s  4475  cbvmptf  4493  cbvmpt  4494  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  opeliunxp  4886  ralxpf  4981  cbviota  5551  csbiota  5575  cbvriota  6262  csbriota  6264  onminex  6634  tfis  6681  findes  6723  abrexex2g  6770  opabex3d  6771  opabex3  6772  abrexex2  6774  dfoprab4f  6851  uzind4s  11219  ac6sf2  28226  esumcvg  28907  bj-sbab  31399  wl-sb8t  31880  wl-sbalnae  31892  wl-ax11-lem8  31922  sbcrexgOLD  35628  pm13.193  36762  opeliun2xp  40167