Theorem nfeq2 2972

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

Syntax hints:   = wceq 1538  Ⅎwnf 1785  Ⅎwnfc 2936

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-nfc 2938

This theorem is referenced by:  issetf  3454  eqvincf  3591  csbhypf  3856  nfpr  4588  intab  4868  nfmpt  5127  cbvmptf  5129  cbvmptfg  5130  zfrepclf  5162  eusvnf  5258  reusv2lem4  5267  reusv2  5269  moop2  5357  elrnmpt1  5794  opabiota  6721  fvmptdf  6751  fmptco  6868  elabrex  6980  nfmpo  7215  cbvmpox  7226  ovmpodxf  7279  zfrep6  7638  fmpox  7747  nfwrecs  7932  erovlem  8376  xpf1o  8663  mapxpen  8667  wdom2d  9028  cnfcom3clem  9152  scott0  9299  cplem2  9303  infxpenc2lem2  9431  acnlem  9459  fin23lem32  9755  hsmexlem2  9838  axcc3  9849  ac6num  9890  lble  11580  nfsum1  15038  nfsum  15039  nfsumOLD  15040  zsum  15067  fsum  15069  fsumcvg2  15076  fsum2dlem  15117  infcvgaux1i  15204  nfcprod1  15256  nfcprod  15257  zprod  15283  fprod  15287  fprodser  15295  fprod2dlem  15326  cayleyhamilton1  21497  neiptopreu  21738  xkocnv  22419  istrkg2ld  26254  cnlnadjlem5  29854  chirred  30178  iundisjf  30352  opabdm  30375  opabrn  30376  dfimafnf  30395  fmptcof2  30420  mpomptxf  30442  f1od2  30483  fpwrelmap  30495  elrspunidl  31014  fedgmullem2  31114  esum2dlem  31461  oms0  31665  bnj1468  32228  bnj981  32332  bnj1463  32437  satfv1  32723  iota5f  33068  nfwlim  33222  nffrecs  33233  bj-seex  34365  isbasisrelowllem1  34772  isbasisrelowllem2  34773  exrecfnlem  34796  finxpreclem6  34813  phpreu  35041  matunitlindflem2  35054  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  mbfposadd  35104  itg2addnclem  35108  cover2  35152  indexa  35171  riotasvd  36252  cdleme31sn1  37677  cdleme32fva  37733  cdlemk36  38209  elnn0rabdioph  39744  wdom2d2  39976  elabrexg  41675  cbvmpo2  41733  cbvmpo1  41734  dffo3f  41806  elrnmptf  41807  disjrnmpt2  41815  fmuldfeqlem1  42224  climf  42264  climf2  42308  cncficcgt0  42530  stoweidlem8  42650  stoweidlem16  42658  stoweidlem19  42661  stoweidlem21  42663  stoweidlem22  42664  stoweidlem23  42665  stoweidlem29  42671  stoweidlem32  42674  stoweidlem35  42677  stoweidlem36  42678  stoweidlem41  42683  stoweidlem44  42686  stoweidlem45  42687  stoweidlem51  42693  stoweidlem53  42695  stoweidlem60  42702  fourierdlem80  42828  sprsymrelf  44012  cbvmpox2  44737  ovmpordxf  44740  1arymaptfo  45057  2arymaptfo  45068