Theorem sbequ12 1993

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 1992	. 2 |- ( x = y -> ( ph -> [ y / x ] ph ) )
2		sbequ2 1742	. 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 1740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-12 1855

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-sb 1741

This theorem is referenced by:  sbequ12r  1994  sbequ12a  1995  sbequ12aOLD  1996  axc16ALT  2106  nfsb4t  2131  sbco2  2159  sb8  2168  sb8e  2169  sbal1  2205  2eu6OLD  2384  clelab  2601  clelabOLD  2602  sbab  2604  cbvralf  3078  cbvralsv  3095  cbvrexsv  3096  cbvrab  3107  sbhypf  3156  mob2  3279  reu2  3287  reu6  3288  sbcralt  3406  sbcrexgOLD  3410  sbcreu  3411  cbvreucsf  3464  cbvrabcsf  3465  csbif  3994  csbifgOLD  3995  rabasiun  4336  cbvopab1  4527  cbvopab1s  4529  cbvmpt  4547  opelopabsb  4766  csbopab  4788  csbopabgALT  4789  opeliunxp  5060  ralxpf  5159  cbviota  5562  csbiota  5586  csbiotagOLD  5587  cbvriota  6268  csbriota  6270  onminex  6641  tfis  6688  findes  6729  abrexex2g  6776  opabex3d  6777  opabex3  6778  abrexex2  6780  dfoprab4f  6857  uzind4s  11166  ac6sf2  27615  cbvmptf  27642  esumcvg  28258  wl-sb8t  30205  wl-sbalnae  30217  wl-ax11-lem8  30237  pm13.193  31522  opeliun2xp  33066  bj-sbab  34513