Theorem nfeq2 2942

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

Syntax hints:   = wceq 1570  Ⅎwnf 1813  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-nfc 2912

This theorem is referenced by:  eqvincf  3609  csbhypf  3881  nfpr  4658  intab  4943  nfmpt  5209  cbvmptf  5211  cbvmptfg  5212  zfrepclf  5252  eusvnf  5363  reusv2lem4  5372  reusv2  5374  moop2  5485  elrnmpt1  5950  opabiota  6963  fvmptdf  6996  dffo3f  7101  fmptco  7125  elabrex  7240  elabrexg  7241  nfmpo  7492  cbvmpox  7503  ovmpodxf  7560  zfrep6OLD  7948  fmpox  8060  nffrecs  8276  erovlem  8807  xpf1o  9123  mapxpen  9127  wdom2d  9538  cnfcom3clem  9670  scott0  9856  cplem2  9872  infxpenc2lem2  10000  acnlem  10028  fin23lem32  10323  hsmexlem2  10406  axcc3  10417  ac6num  10458  lble  12162  nfsum1  15737  nfsum  15738  zsum  15765  fsum  15767  fsumcvg2  15774  fsum2dlem  15817  infcvgaux1i  15907  nfcprod1  15958  nfcprod  15959  zprod  15987  fprod  15991  fprodser  15999  fprod2dlem  16030  cayleyhamilton1  23049  neiptopreu  23290  xkocnv  23971  istrkg2ld  28729  cnlnadjlem5  32423  chirred  32747  iundisjf  32934  opabdm  32956  opabrn  32957  dfimafnf  32981  fmptcof2  33002  mpomptxf  33023  f1od2  33064  fpwrelmap  33078  elrgspnsubrunlem2  33568  elrspunidl  33736  mplvrpmga  33935  esplyfval1  33963  fedgmullem2  34020  esum2dlem  34482  oms0  34687  bnj1468  35234  bnj981  35338  bnj1463  35443  satfv1  35855  iota5f  36216  nfwlim  36312  bj-seex  37557  isbasisrelowllem1  38001  isbasisrelowllem2  38002  exrecfnlem  38025  finxpreclem6  38042  phpreu  38255  matunitlindflem2  38268  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  mbfposadd  38318  itg2addnclem  38322  cover2  38366  indexa  38384  riotasvd  39730  cdleme31sn1  41155  cdleme32fva  41211  cdlemk36  41687  elnn0rabdioph  43530  wdom2d2  43762  permaxrep  45715  permaxsep  45716  cbvmpo2  45815  cbvmpo1  45816  elrnmptf  45899  disjrnmpt2  45906  fmuldfeqlem1  46298  climf  46338  climf2  46380  cncficcgt0  46602  stoweidlem8  46722  stoweidlem16  46730  stoweidlem19  46733  stoweidlem21  46735  stoweidlem22  46736  stoweidlem23  46737  stoweidlem29  46743  stoweidlem32  46746  stoweidlem35  46749  stoweidlem36  46750  stoweidlem41  46755  stoweidlem44  46758  stoweidlem45  46759  stoweidlem51  46765  stoweidlem53  46767  stoweidlem60  46774  fourierdlem80  46900  sprsymrelf  48244  cbvmpox2  49116  ovmpordxf  49119  1arymaptfo  49423  2arymaptfo  49434