Theorem nfeq2 2921

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

Syntax hints:   = wceq 1537  Ⅎwnf 1780  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-cleq 2727  df-nfc 2890

This theorem is referenced by:  eqvincf  3650  csbhypf  3937  nfpr  4697  intab  4983  nfmpt  5255  cbvmptf  5257  cbvmptfg  5258  zfrepclf  5297  eusvnf  5398  reusv2lem4  5407  reusv2  5409  moop2  5512  elrnmpt1  5974  opabiota  6991  fvmptdf  7022  dffo3f  7126  fmptco  7149  elabrex  7262  elabrexg  7263  nfmpo  7515  cbvmpox  7526  ovmpodxf  7583  zfrep6  7978  fmpox  8091  nffrecs  8307  nfwrecsOLD  8341  erovlem  8852  xpf1o  9178  mapxpen  9182  wdom2d  9618  cnfcom3clem  9743  scott0  9924  cplem2  9928  infxpenc2lem2  10058  acnlem  10086  fin23lem32  10382  hsmexlem2  10465  axcc3  10476  ac6num  10517  lble  12218  nfsum1  15723  nfsum  15724  zsum  15751  fsum  15753  fsumcvg2  15760  fsum2dlem  15803  infcvgaux1i  15890  nfcprod1  15941  nfcprod  15942  zprod  15970  fprod  15974  fprodser  15982  fprod2dlem  16013  cayleyhamilton1  22914  neiptopreu  23157  xkocnv  23838  istrkg2ld  28483  cnlnadjlem5  32100  chirred  32424  iundisjf  32609  opabdm  32631  opabrn  32632  dfimafnf  32653  fmptcof2  32674  mpomptxf  32694  f1od2  32739  fpwrelmap  32751  elrspunidl  33436  fedgmullem2  33658  esum2dlem  34073  oms0  34279  bnj1468  34839  bnj981  34943  bnj1463  35048  satfv1  35348  iota5f  35704  nfwlim  35804  bj-seex  36905  isbasisrelowllem1  37338  isbasisrelowllem2  37339  exrecfnlem  37362  finxpreclem6  37379  phpreu  37591  matunitlindflem2  37604  poimirlem24  37631  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  mbfposadd  37654  itg2addnclem  37658  cover2  37702  indexa  37720  riotasvd  38938  cdleme31sn1  40364  cdleme32fva  40420  cdlemk36  40896  elnn0rabdioph  42791  wdom2d2  43024  cbvmpo2  45037  cbvmpo1  45038  elrnmptf  45124  disjrnmpt2  45131  fmuldfeqlem1  45538  climf  45578  climf2  45622  cncficcgt0  45844  stoweidlem8  45964  stoweidlem16  45972  stoweidlem19  45975  stoweidlem21  45977  stoweidlem22  45978  stoweidlem23  45979  stoweidlem29  45985  stoweidlem32  45988  stoweidlem35  45991  stoweidlem36  45992  stoweidlem41  45997  stoweidlem44  46000  stoweidlem45  46001  stoweidlem51  46007  stoweidlem53  46009  stoweidlem60  46016  fourierdlem80  46142  sprsymrelf  47420  cbvmpox2  48181  ovmpordxf  48184  1arymaptfo  48493  2arymaptfo  48504