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 1539  Ⅎwnf 1783  Ⅎwnfc 2881

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-cleq 2722  df-nfc 2883

This theorem is referenced by:  eqvincf  3639  csbhypf  3923  nfpr  4695  intab  4983  nfmpt  5256  cbvmptf  5258  cbvmptfg  5259  zfrepclf  5295  eusvnf  5391  reusv2lem4  5400  reusv2  5402  moop2  5503  elrnmpt1  5958  opabiota  6975  fvmptdf  7005  dffo3f  7108  fmptco  7130  elabrex  7245  elabrexg  7246  nfmpo  7495  cbvmpox  7506  ovmpodxf  7562  zfrep6  7945  fmpox  8057  nffrecs  8272  nfwrecsOLD  8306  erovlem  8811  xpf1o  9143  mapxpen  9147  wdom2d  9579  cnfcom3clem  9704  scott0  9885  cplem2  9889  infxpenc2lem2  10019  acnlem  10047  fin23lem32  10343  hsmexlem2  10426  axcc3  10437  ac6num  10478  lble  12172  nfsum1  15642  nfsum  15643  zsum  15670  fsum  15672  fsumcvg2  15679  fsum2dlem  15722  infcvgaux1i  15809  nfcprod1  15860  nfcprod  15861  zprod  15887  fprod  15891  fprodser  15899  fprod2dlem  15930  cayleyhamilton1  22616  neiptopreu  22859  xkocnv  23540  istrkg2ld  27976  cnlnadjlem5  31589  chirred  31913  iundisjf  32085  opabdm  32105  opabrn  32106  dfimafnf  32125  fmptcof2  32147  mpomptxf  32170  f1od2  32211  fpwrelmap  32223  elrspunidl  32818  fedgmullem2  33001  esum2dlem  33386  oms0  33592  bnj1468  34153  bnj981  34257  bnj1463  34362  satfv1  34650  iota5f  34995  nfwlim  35096  bj-seex  36107  isbasisrelowllem1  36541  isbasisrelowllem2  36542  exrecfnlem  36565  finxpreclem6  36582  phpreu  36777  matunitlindflem2  36790  poimirlem24  36817  poimirlem25  36818  poimirlem26  36819  poimirlem27  36820  mbfposadd  36840  itg2addnclem  36844  cover2  36888  indexa  36906  riotasvd  38131  cdleme31sn1  39557  cdleme32fva  39613  cdlemk36  40089  elnn0rabdioph  41845  wdom2d2  42078  cbvmpo2  44089  cbvmpo1  44090  elrnmptf  44180  disjrnmpt2  44187  fmuldfeqlem1  44598  climf  44638  climf2  44682  cncficcgt0  44904  stoweidlem8  45024  stoweidlem16  45032  stoweidlem19  45035  stoweidlem21  45037  stoweidlem22  45038  stoweidlem23  45039  stoweidlem29  45045  stoweidlem32  45048  stoweidlem35  45051  stoweidlem36  45052  stoweidlem41  45057  stoweidlem44  45060  stoweidlem45  45061  stoweidlem51  45067  stoweidlem53  45069  stoweidlem60  45076  fourierdlem80  45202  sprsymrelf  46463  cbvmpox2  47101  ovmpordxf  47104  1arymaptfo  47418  2arymaptfo  47429