Theorem nfeq2 2944

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2912

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2757  df-nfc 2914

This theorem is used by:  eqvincf  3611  csbhypf  3882  nfpr  4660  intab  4945  nfmpt  5211  cbvmptf  5213  cbvmptfg  5214  zfrepclf  5254  eusvnf  5365  reusv2lem4  5374  reusv2  5376  moop2  5487  elrnmpt1  5952  opabiota  6967  fvmptdf  7000  dffo3f  7105  fmptco  7129  elabrex  7245  elabrexg  7246  nfmpo  7501  cbvmpox  7512  ovmpodxf  7569  zfrep6OLD  7958  fmpox  8070  nffrecs  8286  erovlem  8817  xpf1o  9134  mapxpen  9138  wdom2d  9549  cnfcom3clem  9681  scott0b  9873  scott0OLD  9874  cplem2  9888  cplem2OLD  9889  infxpenc2lem2  10020  acnlem  10048  fin23lem32  10343  hsmexlem2  10426  axcc3  10437  ac6num  10478  lble  12182  nfsum1  15765  nfsum  15766  zsum  15792  fsum  15794  fsumcvg2  15801  fsum2dlem  15844  infcvgaux1i  15934  nfcprod1  15985  nfcprod  15986  zprod  16014  fprod  16018  fprodser  16026  fprod2dlem  16057  cayleyhamilton1  23099  neiptopreu  23340  xkocnv  24022  istrkg2ld  28780  cnlnadjlem5  32494  chirred  32818  iundisjf  33005  opabdm  33027  opabrn  33028  dfimafnf  33052  fmptcof2  33073  mpomptxf  33094  f1od2  33134  fpwrelmap  33148  elrgspnsubrunlem2  33632  elrspunidl  33800  mplvrpmga  33999  esplyfval1  34027  fedgmullem2  34084  esum2dlem  34546  oms0  34752  bnj1468  35299  bnj981  35403  bnj1463  35508  satfv1  35892  iota5f  36253  nfwlim  36349  bj-seex  37614  isbasisrelowllem1  38058  isbasisrelowllem2  38059  exrecfnlem  38082  finxpreclem6  38099  phpreu  38312  matunitlindflem2  38325  poimirlem24  38352  poimirlem25  38353  poimirlem26  38354  poimirlem27  38355  mbfposadd  38375  itg2addnclem  38379  cover2  38424  indexa  38442  riotasvd  39788  cdleme31sn1  41213  cdleme32fva  41269  cdlemk36  41745  elnn0rabdioph  43588  wdom2d2  43820  permaxrep  45773  permaxsep  45774  cbvmpo2  45873  cbvmpo1  45874  elrnmptf  45957  disjrnmpt2  45964  fmuldfeqlem1  46356  climf  46396  climf2  46438  cncficcgt0  46660  stoweidlem8  46780  stoweidlem16  46788  stoweidlem19  46791  stoweidlem21  46793  stoweidlem22  46794  stoweidlem23  46795  stoweidlem29  46801  stoweidlem32  46804  stoweidlem35  46807  stoweidlem36  46808  stoweidlem41  46813  stoweidlem44  46816  stoweidlem45  46817  stoweidlem51  46823  stoweidlem53  46825  stoweidlem60  46832  fourierdlem80  46958  sprsymrelf  48302  cbvmpox2  49173  ovmpordxf  49176  1arymaptfo  49480  2arymaptfo  49491