Theorem nfeq2 2917

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

Syntax hints:   = wceq 1542  Ⅎwnf 1785  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886

This theorem is referenced by:  eqvincf  3593  csbhypf  3866  nfpr  4637  intab  4921  nfmpt  5184  cbvmptf  5186  cbvmptfg  5187  zfrepclf  5227  eusvnf  5330  reusv2lem4  5339  reusv2  5341  moop2  5451  elrnmpt1  5910  opabiota  6917  fvmptdf  6949  dffo3f  7053  fmptco  7077  elabrex  7191  elabrexg  7192  nfmpo  7443  cbvmpox  7454  ovmpodxf  7511  zfrep6OLD  7902  fmpox  8014  nffrecs  8227  erovlem  8754  xpf1o  9071  mapxpen  9075  wdom2d  9489  cnfcom3clem  9620  scott0  9804  cplem2  9808  infxpenc2lem2  9936  acnlem  9964  fin23lem32  10260  hsmexlem2  10343  axcc3  10354  ac6num  10395  lble  12102  nfsum1  15646  nfsum  15647  zsum  15674  fsum  15676  fsumcvg2  15683  fsum2dlem  15726  infcvgaux1i  15816  nfcprod1  15867  nfcprod  15868  zprod  15896  fprod  15900  fprodser  15908  fprod2dlem  15939  cayleyhamilton1  22870  neiptopreu  23111  xkocnv  23792  istrkg2ld  28545  cnlnadjlem5  32160  chirred  32484  iundisjf  32677  opabdm  32702  opabrn  32703  dfimafnf  32727  fmptcof2  32748  mpomptxf  32769  f1od2  32810  fpwrelmap  32824  elrgspnsubrunlem2  33327  elrspunidl  33506  mplvrpmga  33707  esplyfval1  33735  fedgmullem2  33793  esum2dlem  34255  oms0  34460  bnj1468  35007  bnj981  35111  bnj1463  35216  satfv1  35564  iota5f  35925  nfwlim  36021  bj-seex  37248  isbasisrelowllem1  37688  isbasisrelowllem2  37689  exrecfnlem  37712  finxpreclem6  37729  phpreu  37942  matunitlindflem2  37955  poimirlem24  37982  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  mbfposadd  38005  itg2addnclem  38009  cover2  38053  indexa  38071  riotasvd  39419  cdleme31sn1  40844  cdleme32fva  40900  cdlemk36  41376  elnn0rabdioph  43252  wdom2d2  43484  permaxrep  45454  permaxsep  45455  cbvmpo2  45548  cbvmpo1  45549  elrnmptf  45632  disjrnmpt2  45639  fmuldfeqlem1  46033  climf  46073  climf2  46115  cncficcgt0  46337  stoweidlem8  46457  stoweidlem16  46465  stoweidlem19  46468  stoweidlem21  46470  stoweidlem22  46471  stoweidlem23  46472  stoweidlem29  46478  stoweidlem32  46481  stoweidlem35  46484  stoweidlem36  46485  stoweidlem41  46490  stoweidlem44  46493  stoweidlem45  46494  stoweidlem51  46500  stoweidlem53  46502  stoweidlem60  46509  fourierdlem80  46635  sprsymrelf  47970  cbvmpox2  48827  ovmpordxf  48830  1arymaptfo  49134  2arymaptfo  49145