Theorem nfeq2 2943

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2755  df-nfc 2913

This theorem is used by:  eqvincf  3607  csbhypf  3879  nfpr  4654  intab  4943  nfmpt  5209  cbvmptf  5211  cbvmptfg  5212  zfrepclf  5250  eusvnf  5361  reusv2lem4  5370  reusv2  5372  moop2  5481  elrnmpt1  5954  opabiota  6998  fvmptdf  7031  dffo3f  7138  fmptco  7162  elabrex  7277  elabrexg  7278  nfmpo  7533  cbvmpox  7544  ovmpodxf  7602  zfrep6OLD  8001  fmpox  8113  f1od2  8145  nffrecs  8339  erovlem  8872  xpf1o  9196  mapxpen  9200  wdom2d  9611  cnfcom3clem  9743  scott0b  9974  scott0OLD  9975  cplem2  9989  cplem2OLD  9990  infxpenc2lem2  10138  acnlem  10166  fin23lem32  10461  hsmexlem2  10544  axcc3  10555  ac6num  10596  lble  12309  nfsum1  15901  nfsum  15902  zsum  15928  fsum  15930  fsumcvg2  15937  fsum2dlem  15980  infcvgaux1i  16070  nfcprod1  16121  nfcprod  16122  zprod  16148  fprod  16152  fprodser  16160  fprod2dlem  16191  matunitlindflem2  23050  cayleyhamilton1  23265  neiptopreu  23506  xkocnv  24188  istrkg2ld  28979  cnlnadjlem5  32730  chirred  33054  iundisjf  33281  opabdm  33303  opabrn  33304  dfimafnf  33328  fmptcof2  33349  mpomptxf  33369  fpwrelmap  33421  elrgspnsubrunlem2  33908  elrspunidl  34082  mplvrpmga  34288  esplyfval1  34316  fedgmullem2  34373  esum2dlem  34835  oms0  35040  bnj1468  35587  bnj981  35691  bnj1463  35796  srepdflem2  36127  satfv1  36336  iota5f  36704  nfwlim  36799  bj-seex  38049  isbasisrelowllem1  38546  isbasisrelowllem2  38547  exrecfnlem  38570  finxpreclem6  38587  phpreu  38795  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  mbfposadd  38853  itg2addnclem  38857  cover2  38917  indexa  38935  riotasvd  40279  cdleme31sn1  41704  cdleme32fva  41760  cdlemk36  42236  elnn0rabdioph  44076  wdom2d2  44308  permaxrep  46260  permaxsep  46261  cbvmpo2  46385  cbvmpo1  46386  elrnmptf  46469  disjrnmpt2  46476  fmuldfeqlem1  46867  climf  46907  climf2  46949  cncficcgt0  47171  stoweidlem8  47291  stoweidlem16  47299  stoweidlem19  47302  stoweidlem21  47304  stoweidlem22  47305  stoweidlem23  47306  stoweidlem29  47312  stoweidlem32  47315  stoweidlem35  47318  stoweidlem36  47319  stoweidlem41  47324  stoweidlem44  47327  stoweidlem45  47328  stoweidlem51  47334  stoweidlem53  47336  stoweidlem60  47343  fourierdlem80  47469  sprsymrelf  48850  cbvmpox2  49779  ovmpordxf  49782  1arymaptfo  50086  2arymaptfo  50097