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  3616  csbhypf  3890  nfpr  4656  intab  4942  nfmpt  5205  cbvmptf  5207  cbvmptfg  5208  zfrepclf  5246  eusvnf  5347  reusv2lem4  5356  reusv2  5358  moop2  5462  elrnmpt1  5924  opabiota  6943  fvmptdf  6974  dffo3f  7078  fmptco  7101  elabrex  7216  elabrexg  7217  nfmpo  7471  cbvmpox  7482  ovmpodxf  7539  zfrep6  7933  fmpox  8046  nffrecs  8262  erovlem  8786  xpf1o  9103  mapxpen  9107  wdom2d  9533  cnfcom3clem  9658  scott0  9839  cplem2  9843  infxpenc2lem2  9973  acnlem  10001  fin23lem32  10297  hsmexlem2  10380  axcc3  10391  ac6num  10432  lble  12135  nfsum1  15656  nfsum  15657  zsum  15684  fsum  15686  fsumcvg2  15693  fsum2dlem  15736  infcvgaux1i  15823  nfcprod1  15874  nfcprod  15875  zprod  15903  fprod  15907  fprodser  15915  fprod2dlem  15946  cayleyhamilton1  22779  neiptopreu  23020  xkocnv  23701  istrkg2ld  28387  cnlnadjlem5  32000  chirred  32324  iundisjf  32518  opabdm  32539  opabrn  32540  dfimafnf  32560  fmptcof2  32581  mpomptxf  32601  f1od2  32644  fpwrelmap  32656  elrgspnsubrunlem2  33199  elrspunidl  33399  fedgmullem2  33626  esum2dlem  34082  oms0  34288  bnj1468  34836  bnj981  34940  bnj1463  35045  satfv1  35350  iota5f  35711  nfwlim  35810  bj-seex  36910  isbasisrelowllem1  37343  isbasisrelowllem2  37344  exrecfnlem  37367  finxpreclem6  37384  phpreu  37598  matunitlindflem2  37611  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  mbfposadd  37661  itg2addnclem  37665  cover2  37709  indexa  37727  riotasvd  38949  cdleme31sn1  40375  cdleme32fva  40431  cdlemk36  40907  elnn0rabdioph  42791  wdom2d2  43024  permaxrep  44996  permaxsep  44997  cbvmpo2  45091  cbvmpo1  45092  elrnmptf  45175  disjrnmpt2  45182  fmuldfeqlem1  45580  climf  45620  climf2  45664  cncficcgt0  45886  stoweidlem8  46006  stoweidlem16  46014  stoweidlem19  46017  stoweidlem21  46019  stoweidlem22  46020  stoweidlem23  46021  stoweidlem29  46027  stoweidlem32  46030  stoweidlem35  46033  stoweidlem36  46034  stoweidlem41  46039  stoweidlem44  46042  stoweidlem45  46043  stoweidlem51  46049  stoweidlem53  46051  stoweidlem60  46058  fourierdlem80  46184  sprsymrelf  47496  cbvmpox2  48324  ovmpordxf  48327  1arymaptfo  48632  2arymaptfo  48643