Theorem nfeq2 2916

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

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

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 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2727  df-nfc 2885

This theorem is referenced by:  eqvincf  3629  csbhypf  3902  nfpr  4668  intab  4954  nfmpt  5219  cbvmptf  5221  cbvmptfg  5222  zfrepclf  5261  eusvnf  5362  reusv2lem4  5371  reusv2  5373  moop2  5477  elrnmpt1  5940  opabiota  6961  fvmptdf  6992  dffo3f  7096  fmptco  7119  elabrex  7234  elabrexg  7235  nfmpo  7489  cbvmpox  7500  ovmpodxf  7557  zfrep6  7953  fmpox  8066  nffrecs  8282  nfwrecsOLD  8316  erovlem  8827  xpf1o  9153  mapxpen  9157  wdom2d  9594  cnfcom3clem  9719  scott0  9900  cplem2  9904  infxpenc2lem2  10034  acnlem  10062  fin23lem32  10358  hsmexlem2  10441  axcc3  10452  ac6num  10493  lble  12194  nfsum1  15706  nfsum  15707  zsum  15734  fsum  15736  fsumcvg2  15743  fsum2dlem  15786  infcvgaux1i  15873  nfcprod1  15924  nfcprod  15925  zprod  15953  fprod  15957  fprodser  15965  fprod2dlem  15996  cayleyhamilton1  22830  neiptopreu  23071  xkocnv  23752  istrkg2ld  28439  cnlnadjlem5  32052  chirred  32376  iundisjf  32570  opabdm  32591  opabrn  32592  dfimafnf  32614  fmptcof2  32635  mpomptxf  32655  f1od2  32698  fpwrelmap  32710  elrgspnsubrunlem2  33243  elrspunidl  33443  fedgmullem2  33670  esum2dlem  34123  oms0  34329  bnj1468  34877  bnj981  34981  bnj1463  35086  satfv1  35385  iota5f  35741  nfwlim  35840  bj-seex  36940  isbasisrelowllem1  37373  isbasisrelowllem2  37374  exrecfnlem  37397  finxpreclem6  37414  phpreu  37628  matunitlindflem2  37641  poimirlem24  37668  poimirlem25  37669  poimirlem26  37670  poimirlem27  37671  mbfposadd  37691  itg2addnclem  37695  cover2  37739  indexa  37757  riotasvd  38974  cdleme31sn1  40400  cdleme32fva  40456  cdlemk36  40932  elnn0rabdioph  42826  wdom2d2  43059  permaxrep  45031  permaxsep  45032  cbvmpo2  45121  cbvmpo1  45122  elrnmptf  45205  disjrnmpt2  45212  fmuldfeqlem1  45611  climf  45651  climf2  45695  cncficcgt0  45917  stoweidlem8  46037  stoweidlem16  46045  stoweidlem19  46048  stoweidlem21  46050  stoweidlem22  46051  stoweidlem23  46052  stoweidlem29  46058  stoweidlem32  46061  stoweidlem35  46064  stoweidlem36  46065  stoweidlem41  46070  stoweidlem44  46073  stoweidlem45  46074  stoweidlem51  46080  stoweidlem53  46082  stoweidlem60  46089  fourierdlem80  46215  sprsymrelf  47509  cbvmpox2  48311  ovmpordxf  48314  1arymaptfo  48623  2arymaptfo  48634