Theorem nfeq2 2912

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq2.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq2	⊢ Ⅎ𝑥 𝐴 = 𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2

Step	Hyp	Ref	Expression
1		nfcv 2894	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2908	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-nfc 2881

This theorem is referenced by:  eqvincf  3600  csbhypf  3873  nfpr  4642  intab  4926  nfmpt  5187  cbvmptf  5189  cbvmptfg  5190  zfrepclf  5227  eusvnf  5328  reusv2lem4  5337  reusv2  5339  moop2  5440  elrnmpt1  5899  opabiota  6904  fvmptdf  6935  dffo3f  7039  fmptco  7062  elabrex  7176  elabrexg  7177  nfmpo  7428  cbvmpox  7439  ovmpodxf  7496  zfrep6  7887  fmpox  7999  nffrecs  8213  erovlem  8737  xpf1o  9052  mapxpen  9056  wdom2d  9466  cnfcom3clem  9595  scott0  9779  cplem2  9783  infxpenc2lem2  9911  acnlem  9939  fin23lem32  10235  hsmexlem2  10318  axcc3  10329  ac6num  10370  lble  12074  nfsum1  15597  nfsum  15598  zsum  15625  fsum  15627  fsumcvg2  15634  fsum2dlem  15677  infcvgaux1i  15764  nfcprod1  15815  nfcprod  15816  zprod  15844  fprod  15848  fprodser  15856  fprod2dlem  15887  cayleyhamilton1  22807  neiptopreu  23048  xkocnv  23729  istrkg2ld  28438  cnlnadjlem5  32051  chirred  32375  iundisjf  32569  opabdm  32594  opabrn  32595  dfimafnf  32618  fmptcof2  32639  mpomptxf  32659  f1od2  32702  fpwrelmap  32716  elrgspnsubrunlem2  33215  elrspunidl  33393  mplvrpmga  33575  fedgmullem2  33643  esum2dlem  34105  oms0  34310  bnj1468  34858  bnj981  34962  bnj1463  35067  satfv1  35407  iota5f  35768  nfwlim  35864  bj-seex  36964  isbasisrelowllem1  37397  isbasisrelowllem2  37398  exrecfnlem  37421  finxpreclem6  37438  phpreu  37652  matunitlindflem2  37665  poimirlem24  37692  poimirlem25  37693  poimirlem26  37694  poimirlem27  37695  mbfposadd  37715  itg2addnclem  37719  cover2  37763  indexa  37781  riotasvd  39003  cdleme31sn1  40428  cdleme32fva  40484  cdlemk36  40960  elnn0rabdioph  42844  wdom2d2  43076  permaxrep  45047  permaxsep  45048  cbvmpo2  45142  cbvmpo1  45143  elrnmptf  45226  disjrnmpt2  45233  fmuldfeqlem1  45630  climf  45670  climf2  45712  cncficcgt0  45934  stoweidlem8  46054  stoweidlem16  46062  stoweidlem19  46065  stoweidlem21  46067  stoweidlem22  46068  stoweidlem23  46069  stoweidlem29  46075  stoweidlem32  46078  stoweidlem35  46081  stoweidlem36  46082  stoweidlem41  46087  stoweidlem44  46090  stoweidlem45  46091  stoweidlem51  46097  stoweidlem53  46099  stoweidlem60  46106  fourierdlem80  46232  sprsymrelf  47534  cbvmpox2  48375  ovmpordxf  48378  1arymaptfo  48683  2arymaptfo  48694