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 1542  Ⅎwnf 1785  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2728  df-nfc 2885

This theorem is referenced by:  eqvincf  3592  csbhypf  3865  nfpr  4636  intab  4920  nfmpt  5183  cbvmptf  5185  cbvmptfg  5186  zfrepclf  5226  eusvnf  5334  reusv2lem4  5343  reusv2  5345  moop2  5456  elrnmpt1  5915  opabiota  6922  fvmptdf  6954  dffo3f  7058  fmptco  7082  elabrex  7197  elabrexg  7198  nfmpo  7449  cbvmpox  7460  ovmpodxf  7517  zfrep6OLD  7908  fmpox  8020  nffrecs  8233  erovlem  8760  xpf1o  9077  mapxpen  9081  wdom2d  9495  cnfcom3clem  9626  scott0  9810  cplem2  9814  infxpenc2lem2  9942  acnlem  9970  fin23lem32  10266  hsmexlem2  10349  axcc3  10360  ac6num  10401  lble  12108  nfsum1  15652  nfsum  15653  zsum  15680  fsum  15682  fsumcvg2  15689  fsum2dlem  15732  infcvgaux1i  15822  nfcprod1  15873  nfcprod  15874  zprod  15902  fprod  15906  fprodser  15914  fprod2dlem  15945  cayleyhamilton1  22857  neiptopreu  23098  xkocnv  23779  istrkg2ld  28528  cnlnadjlem5  32142  chirred  32466  iundisjf  32659  opabdm  32684  opabrn  32685  dfimafnf  32709  fmptcof2  32730  mpomptxf  32751  f1od2  32792  fpwrelmap  32806  elrgspnsubrunlem2  33309  elrspunidl  33488  mplvrpmga  33689  esplyfval1  33717  fedgmullem2  33774  esum2dlem  34236  oms0  34441  bnj1468  34988  bnj981  35092  bnj1463  35197  satfv1  35545  iota5f  35906  nfwlim  36002  bj-seex  37229  isbasisrelowllem1  37671  isbasisrelowllem2  37672  exrecfnlem  37695  finxpreclem6  37712  phpreu  37925  matunitlindflem2  37938  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  mbfposadd  37988  itg2addnclem  37992  cover2  38036  indexa  38054  riotasvd  39402  cdleme31sn1  40827  cdleme32fva  40883  cdlemk36  41359  elnn0rabdioph  43231  wdom2d2  43463  permaxrep  45433  permaxsep  45434  cbvmpo2  45527  cbvmpo1  45528  elrnmptf  45611  disjrnmpt2  45618  fmuldfeqlem1  46012  climf  46052  climf2  46094  cncficcgt0  46316  stoweidlem8  46436  stoweidlem16  46444  stoweidlem19  46447  stoweidlem21  46449  stoweidlem22  46450  stoweidlem23  46451  stoweidlem29  46457  stoweidlem32  46460  stoweidlem35  46463  stoweidlem36  46464  stoweidlem41  46469  stoweidlem44  46472  stoweidlem45  46473  stoweidlem51  46479  stoweidlem53  46481  stoweidlem60  46488  fourierdlem80  46614  sprsymrelf  47955  cbvmpox2  48812  ovmpordxf  48815  1arymaptfo  49119  2arymaptfo  49130