Theorem nfeq2 2909

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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2905	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by:  eqvincf  3613  csbhypf  3887  nfpr  4652  intab  4938  nfmpt  5200  cbvmptf  5202  cbvmptfg  5203  zfrepclf  5241  eusvnf  5342  reusv2lem4  5351  reusv2  5353  moop2  5457  elrnmpt1  5913  opabiota  6925  fvmptdf  6956  dffo3f  7060  fmptco  7083  elabrex  7198  elabrexg  7199  nfmpo  7451  cbvmpox  7462  ovmpodxf  7519  zfrep6  7913  fmpox  8025  nffrecs  8239  erovlem  8763  xpf1o  9080  mapxpen  9084  wdom2d  9509  cnfcom3clem  9634  scott0  9815  cplem2  9819  infxpenc2lem2  9949  acnlem  9977  fin23lem32  10273  hsmexlem2  10356  axcc3  10367  ac6num  10408  lble  12111  nfsum1  15632  nfsum  15633  zsum  15660  fsum  15662  fsumcvg2  15669  fsum2dlem  15712  infcvgaux1i  15799  nfcprod1  15850  nfcprod  15851  zprod  15879  fprod  15883  fprodser  15891  fprod2dlem  15922  cayleyhamilton1  22755  neiptopreu  22996  xkocnv  23677  istrkg2ld  28363  cnlnadjlem5  31973  chirred  32297  iundisjf  32491  opabdm  32512  opabrn  32513  dfimafnf  32533  fmptcof2  32554  mpomptxf  32574  f1od2  32617  fpwrelmap  32629  elrgspnsubrunlem2  33172  elrspunidl  33372  fedgmullem2  33599  esum2dlem  34055  oms0  34261  bnj1468  34809  bnj981  34913  bnj1463  35018  satfv1  35323  iota5f  35684  nfwlim  35783  bj-seex  36883  isbasisrelowllem1  37316  isbasisrelowllem2  37317  exrecfnlem  37340  finxpreclem6  37357  phpreu  37571  matunitlindflem2  37584  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  mbfposadd  37634  itg2addnclem  37638  cover2  37682  indexa  37700  riotasvd  38922  cdleme31sn1  40348  cdleme32fva  40404  cdlemk36  40880  elnn0rabdioph  42764  wdom2d2  42997  permaxrep  44969  permaxsep  44970  cbvmpo2  45064  cbvmpo1  45065  elrnmptf  45148  disjrnmpt2  45155  fmuldfeqlem1  45553  climf  45593  climf2  45637  cncficcgt0  45859  stoweidlem8  45979  stoweidlem16  45987  stoweidlem19  45990  stoweidlem21  45992  stoweidlem22  45993  stoweidlem23  45994  stoweidlem29  46000  stoweidlem32  46003  stoweidlem35  46006  stoweidlem36  46007  stoweidlem41  46012  stoweidlem44  46015  stoweidlem45  46016  stoweidlem51  46022  stoweidlem53  46024  stoweidlem60  46031  fourierdlem80  46157  sprsymrelf  47469  cbvmpox2  48297  ovmpordxf  48300  1arymaptfo  48605  2arymaptfo  48616