Theorem sbequ12 1992

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
sbequ12

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1991	. 2
2		sbequ2 1741	. 2
3	1, 2	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184  [wsb 1739

This theorem is referenced by:  sbequ12r  1993  sbequ12a  1994  sbequ12aOLD  1995  axc16ALT  2105  nfsb4t  2130  sbco2  2158  sb8  2167  sb8e  2168  sbal1  2204  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  3408  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  cbvreucsf  3468  cbvrabcsf  3469  csbif  3991  csbifgOLD  3992  rabasiun  4334  cbvopab1  4522  cbvopab1s  4524  cbvmpt  4542  opelopabsb  4762  csbopab  4784  csbopabgALT  4785  opeliunxp  5056  ralxpf  5154  cbviota  5561  csbiota  5585  csbiotagOLD  5586  cbvriota  6267  csbriota  6269  onminex  6642  tfis  6689  findes  6730  abrexex2g  6777  opabex3d  6778  opabex3  6779  abrexex2  6781  dfoprab4f  6858  uzind4s  11170  cbvmptf  27494  esumcvg  28092  wl-sb8t  30000  wl-sbalnae  30012  wl-ax11-lem8  30032  pm13.193  31318  opeliun2xp  32922  bj-sbab  34370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740