Theorem nfeq2 2909

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by:  eqvincf  3605  csbhypf  3879  nfpr  4644  intab  4928  nfmpt  5190  cbvmptf  5192  cbvmptfg  5193  zfrepclf  5230  eusvnf  5331  reusv2lem4  5340  reusv2  5342  moop2  5445  elrnmpt1  5902  opabiota  6905  fvmptdf  6936  dffo3f  7040  fmptco  7063  elabrex  7178  elabrexg  7179  nfmpo  7431  cbvmpox  7442  ovmpodxf  7499  zfrep6  7890  fmpox  8002  nffrecs  8216  erovlem  8740  xpf1o  9056  mapxpen  9060  wdom2d  9472  cnfcom3clem  9601  scott0  9782  cplem2  9786  infxpenc2lem2  9914  acnlem  9942  fin23lem32  10238  hsmexlem2  10321  axcc3  10332  ac6num  10373  lble  12077  nfsum1  15597  nfsum  15598  zsum  15625  fsum  15627  fsumcvg2  15634  fsum2dlem  15677  infcvgaux1i  15764  nfcprod1  15815  nfcprod  15816  zprod  15844  fprod  15848  fprodser  15856  fprod2dlem  15887  cayleyhamilton1  22777  neiptopreu  23018  xkocnv  23699  istrkg2ld  28405  cnlnadjlem5  32015  chirred  32339  iundisjf  32533  opabdm  32556  opabrn  32557  dfimafnf  32579  fmptcof2  32600  mpomptxf  32620  f1od2  32663  fpwrelmap  32676  elrgspnsubrunlem2  33188  elrspunidl  33365  mplvrpmga  33546  fedgmullem2  33597  esum2dlem  34059  oms0  34265  bnj1468  34813  bnj981  34917  bnj1463  35022  satfv1  35336  iota5f  35697  nfwlim  35796  bj-seex  36896  isbasisrelowllem1  37329  isbasisrelowllem2  37330  exrecfnlem  37353  finxpreclem6  37370  phpreu  37584  matunitlindflem2  37597  poimirlem24  37624  poimirlem25  37625  poimirlem26  37626  poimirlem27  37627  mbfposadd  37647  itg2addnclem  37651  cover2  37695  indexa  37713  riotasvd  38935  cdleme31sn1  40360  cdleme32fva  40416  cdlemk36  40892  elnn0rabdioph  42776  wdom2d2  43008  permaxrep  44980  permaxsep  44981  cbvmpo2  45075  cbvmpo1  45076  elrnmptf  45159  disjrnmpt2  45166  fmuldfeqlem1  45563  climf  45603  climf2  45647  cncficcgt0  45869  stoweidlem8  45989  stoweidlem16  45997  stoweidlem19  46000  stoweidlem21  46002  stoweidlem22  46003  stoweidlem23  46004  stoweidlem29  46010  stoweidlem32  46013  stoweidlem35  46016  stoweidlem36  46017  stoweidlem41  46022  stoweidlem44  46025  stoweidlem45  46026  stoweidlem51  46032  stoweidlem53  46034  stoweidlem60  46041  fourierdlem80  46167  sprsymrelf  47479  cbvmpox2  48320  ovmpordxf  48323  1arymaptfo  48628  2arymaptfo  48639