Theorem nfeq2 2939

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2752  df-nfc 2909

This theorem is used by:  eqvincf  3604  csbhypf  3875  nfpr  4653  intab  4938  nfmpt  5203  cbvmptf  5205  cbvmptfg  5206  zfrepclf  5246  eusvnf  5357  reusv2lem4  5366  reusv2  5368  moop2  5479  elrnmpt1  5944  opabiota  6960  fvmptdf  6993  dffo3f  7099  fmptco  7123  elabrex  7239  elabrexg  7240  nfmpo  7495  cbvmpox  7506  ovmpodxf  7563  zfrep6OLD  7952  fmpox  8064  nffrecs  8282  erovlem  8813  xpf1o  9137  mapxpen  9141  wdom2d  9552  cnfcom3clem  9684  scott0b  9876  scott0OLD  9877  cplem2  9891  cplem2OLD  9892  infxpenc2lem2  10023  acnlem  10051  fin23lem32  10346  hsmexlem2  10429  axcc3  10440  ac6num  10481  lble  12191  nfsum1  15777  nfsum  15778  zsum  15804  fsum  15806  fsumcvg2  15813  fsum2dlem  15856  infcvgaux1i  15946  nfcprod1  15997  nfcprod  15998  zprod  16024  fprod  16028  fprodser  16036  fprod2dlem  16067  matunitlindflem2  22902  cayleyhamilton1  23117  neiptopreu  23358  xkocnv  24040  istrkg2ld  28801  cnlnadjlem5  32552  chirred  32876  iundisjf  33062  opabdm  33084  opabrn  33085  dfimafnf  33109  fmptcof2  33130  mpomptxf  33151  f1od2  33190  fpwrelmap  33204  elrgspnsubrunlem2  33688  elrspunidl  33856  mplvrpmga  34055  esplyfval1  34083  fedgmullem2  34140  esum2dlem  34602  oms0  34808  bnj1468  35355  bnj981  35459  bnj1463  35564  satfv1  35942  iota5f  36303  nfwlim  36399  bj-seex  37665  isbasisrelowllem1  38109  isbasisrelowllem2  38110  exrecfnlem  38133  finxpreclem6  38150  phpreu  38358  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  mbfposadd  38416  itg2addnclem  38420  cover2  38465  indexa  38483  riotasvd  39829  cdleme31sn1  41254  cdleme32fva  41310  cdlemk36  41786  elnn0rabdioph  43644  wdom2d2  43876  permaxrep  45829  permaxsep  45830  cbvmpo2  45929  cbvmpo1  45930  elrnmptf  46013  disjrnmpt2  46020  fmuldfeqlem1  46412  climf  46452  climf2  46494  cncficcgt0  46716  stoweidlem8  46836  stoweidlem16  46844  stoweidlem19  46847  stoweidlem21  46849  stoweidlem22  46850  stoweidlem23  46851  stoweidlem29  46857  stoweidlem32  46860  stoweidlem35  46863  stoweidlem36  46864  stoweidlem41  46869  stoweidlem44  46872  stoweidlem45  46873  stoweidlem51  46879  stoweidlem53  46881  stoweidlem60  46888  fourierdlem80  47014  sprsymrelf  48395  cbvmpox2  49266  ovmpordxf  49269  1arymaptfo  49573  2arymaptfo  49584