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 1541  Ⅎwnf 1784  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-nfc 2885

This theorem is referenced by:  eqvincf  3604  csbhypf  3877  nfpr  4649  intab  4933  nfmpt  5196  cbvmptf  5198  cbvmptfg  5199  zfrepclf  5236  eusvnf  5337  reusv2lem4  5346  reusv2  5348  moop2  5450  elrnmpt1  5909  opabiota  6916  fvmptdf  6947  dffo3f  7051  fmptco  7074  elabrex  7188  elabrexg  7189  nfmpo  7440  cbvmpox  7451  ovmpodxf  7508  zfrep6  7899  fmpox  8011  nffrecs  8225  erovlem  8750  xpf1o  9067  mapxpen  9071  wdom2d  9485  cnfcom3clem  9614  scott0  9798  cplem2  9802  infxpenc2lem2  9930  acnlem  9958  fin23lem32  10254  hsmexlem2  10337  axcc3  10348  ac6num  10389  lble  12094  nfsum1  15613  nfsum  15614  zsum  15641  fsum  15643  fsumcvg2  15650  fsum2dlem  15693  infcvgaux1i  15780  nfcprod1  15831  nfcprod  15832  zprod  15860  fprod  15864  fprodser  15872  fprod2dlem  15903  cayleyhamilton1  22836  neiptopreu  23077  xkocnv  23758  istrkg2ld  28532  cnlnadjlem5  32146  chirred  32470  iundisjf  32664  opabdm  32689  opabrn  32690  dfimafnf  32714  fmptcof2  32735  mpomptxf  32757  f1od2  32798  fpwrelmap  32812  elrgspnsubrunlem2  33330  elrspunidl  33509  mplvrpmga  33710  fedgmullem2  33787  esum2dlem  34249  oms0  34454  bnj1468  35002  bnj981  35106  bnj1463  35211  satfv1  35557  iota5f  35918  nfwlim  36014  bj-seex  37123  isbasisrelowllem1  37560  isbasisrelowllem2  37561  exrecfnlem  37584  finxpreclem6  37601  phpreu  37805  matunitlindflem2  37818  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  mbfposadd  37868  itg2addnclem  37872  cover2  37916  indexa  37934  riotasvd  39216  cdleme31sn1  40641  cdleme32fva  40697  cdlemk36  41173  elnn0rabdioph  43045  wdom2d2  43277  permaxrep  45247  permaxsep  45248  cbvmpo2  45341  cbvmpo1  45342  elrnmptf  45425  disjrnmpt2  45432  fmuldfeqlem1  45828  climf  45868  climf2  45910  cncficcgt0  46132  stoweidlem8  46252  stoweidlem16  46260  stoweidlem19  46263  stoweidlem21  46265  stoweidlem22  46266  stoweidlem23  46267  stoweidlem29  46273  stoweidlem32  46276  stoweidlem35  46279  stoweidlem36  46280  stoweidlem41  46285  stoweidlem44  46288  stoweidlem45  46289  stoweidlem51  46295  stoweidlem53  46297  stoweidlem60  46304  fourierdlem80  46430  sprsymrelf  47741  cbvmpox2  48582  ovmpordxf  48585  1arymaptfo  48889  2arymaptfo  48900