Theorem nfeq2 2918

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

Syntax hints:   = wceq 1547  Ⅎwnf 1790  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-nfc 2888

This theorem is referenced by:  eqvincf  3588  csbhypf  3859  nfpr  4624  intab  4908  nfmpt  5170  cbvmptf  5172  cbvmptfg  5173  zfrepclf  5213  eusvnf  5321  reusv2lem4  5330  reusv2  5332  moop2  5443  elrnmpt1  5902  opabiota  6909  fvmptdf  6942  dffo3f  7047  fmptco  7071  elabrex  7186  elabrexg  7187  nfmpo  7438  cbvmpox  7449  ovmpodxf  7506  zfrep6OLD  7897  fmpox  8009  nffrecs  8223  erovlem  8750  xpf1o  9067  mapxpen  9071  wdom2d  9485  cnfcom3clem  9617  scott0  9801  cplem2  9805  infxpenc2lem2  9933  acnlem  9961  fin23lem32  10257  hsmexlem2  10340  axcc3  10351  ac6num  10392  lble  12099  nfsum1  15643  nfsum  15644  zsum  15671  fsum  15673  fsumcvg2  15680  fsum2dlem  15723  infcvgaux1i  15813  nfcprod1  15864  nfcprod  15865  zprod  15893  fprod  15897  fprodser  15905  fprod2dlem  15936  cayleyhamilton1  22875  neiptopreu  23116  xkocnv  23797  istrkg2ld  28546  cnlnadjlem5  32160  chirred  32484  iundisjf  32678  opabdm  32703  opabrn  32704  dfimafnf  32728  fmptcof2  32749  mpomptxf  32770  f1od2  32811  fpwrelmap  32825  elrgspnsubrunlem2  33329  elrspunidl  33511  mplvrpmga  33729  esplyfval1  33757  fedgmullem2  33814  esum2dlem  34276  oms0  34481  bnj1468  35028  bnj981  35132  bnj1463  35237  satfv1  35591  iota5f  35952  nfwlim  36048  bj-seex  37275  isbasisrelowllem1  37717  isbasisrelowllem2  37718  exrecfnlem  37741  finxpreclem6  37758  phpreu  37971  matunitlindflem2  37984  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  mbfposadd  38034  itg2addnclem  38038  cover2  38082  indexa  38100  riotasvd  39448  cdleme31sn1  40873  cdleme32fva  40929  cdlemk36  41405  elnn0rabdioph  43248  wdom2d2  43480  permaxrep  45450  permaxsep  45451  cbvmpo2  45544  cbvmpo1  45545  elrnmptf  45628  disjrnmpt2  45635  fmuldfeqlem1  46027  climf  46067  climf2  46109  cncficcgt0  46331  stoweidlem8  46451  stoweidlem16  46459  stoweidlem19  46462  stoweidlem21  46464  stoweidlem22  46465  stoweidlem23  46466  stoweidlem29  46472  stoweidlem32  46475  stoweidlem35  46478  stoweidlem36  46479  stoweidlem41  46484  stoweidlem44  46487  stoweidlem45  46488  stoweidlem51  46494  stoweidlem53  46496  stoweidlem60  46503  fourierdlem80  46629  sprsymrelf  47970  cbvmpox2  48827  ovmpordxf  48830  1arymaptfo  49134  2arymaptfo  49145