Theorem nfeq2 2917

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

Syntax hints:   = wceq 1542  Ⅎwnf 1785  Ⅎwnfc 2884

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 2709

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 2729  df-nfc 2886

This theorem is referenced by:  eqvincf  3606  csbhypf  3879  nfpr  4651  intab  4935  nfmpt  5198  cbvmptf  5200  cbvmptfg  5201  zfrepclf  5238  eusvnf  5339  reusv2lem4  5348  reusv2  5350  moop2  5458  elrnmpt1  5917  opabiota  6924  fvmptdf  6956  dffo3f  7060  fmptco  7084  elabrex  7198  elabrexg  7199  nfmpo  7450  cbvmpox  7461  ovmpodxf  7518  zfrep6  7909  fmpox  8021  nffrecs  8235  erovlem  8762  xpf1o  9079  mapxpen  9083  wdom2d  9497  cnfcom3clem  9626  scott0  9810  cplem2  9814  infxpenc2lem2  9942  acnlem  9970  fin23lem32  10266  hsmexlem2  10349  axcc3  10360  ac6num  10401  lble  12106  nfsum1  15625  nfsum  15626  zsum  15653  fsum  15655  fsumcvg2  15662  fsum2dlem  15705  infcvgaux1i  15792  nfcprod1  15843  nfcprod  15844  zprod  15872  fprod  15876  fprodser  15884  fprod2dlem  15915  cayleyhamilton1  22848  neiptopreu  23089  xkocnv  23770  istrkg2ld  28544  cnlnadjlem5  32159  chirred  32483  iundisjf  32676  opabdm  32701  opabrn  32702  dfimafnf  32726  fmptcof2  32747  mpomptxf  32768  f1od2  32809  fpwrelmap  32823  elrgspnsubrunlem2  33342  elrspunidl  33521  mplvrpmga  33722  esplyfval1  33750  fedgmullem2  33808  esum2dlem  34270  oms0  34475  bnj1468  35022  bnj981  35126  bnj1463  35231  satfv1  35579  iota5f  35940  nfwlim  36036  bj-seex  37170  isbasisrelowllem1  37610  isbasisrelowllem2  37611  exrecfnlem  37634  finxpreclem6  37651  phpreu  37855  matunitlindflem2  37868  poimirlem24  37895  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  mbfposadd  37918  itg2addnclem  37922  cover2  37966  indexa  37984  riotasvd  39332  cdleme31sn1  40757  cdleme32fva  40813  cdlemk36  41289  elnn0rabdioph  43160  wdom2d2  43392  permaxrep  45362  permaxsep  45363  cbvmpo2  45456  cbvmpo1  45457  elrnmptf  45540  disjrnmpt2  45547  fmuldfeqlem1  45942  climf  45982  climf2  46024  cncficcgt0  46246  stoweidlem8  46366  stoweidlem16  46374  stoweidlem19  46377  stoweidlem21  46379  stoweidlem22  46380  stoweidlem23  46381  stoweidlem29  46387  stoweidlem32  46390  stoweidlem35  46393  stoweidlem36  46394  stoweidlem41  46399  stoweidlem44  46402  stoweidlem45  46403  stoweidlem51  46409  stoweidlem53  46411  stoweidlem60  46418  fourierdlem80  46544  sprsymrelf  47855  cbvmpox2  48696  ovmpordxf  48699  1arymaptfo  49003  2arymaptfo  49014