Theorem nfeq1 2634

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1

Assertion

Ref	Expression
nfeq1

Distinct variable group:   ,

Proof of Theorem nfeq1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2
2		nfcv 2619	. 2
3	1, 2	nfeq 2630	1

Syntax hints:  =wceq 1395  F/wnf 1616  F/_wnfc 2605

This theorem is referenced by:  euabsn  4102  disjxun  4450  reusv6OLD  4663  opabiotafun  5934  fvmptt  5971  eusvobj2  6289  oprabv  6345  ovmpt2dv2  6436  ov3  6439  dom2lem  7575  pwfseqlem2  9058  fsumf1o  13545  isummulc2  13577  fsum00  13612  isumshft  13651  zprod  13744  fprodf1o  13753  prodss  13754  iserodd  14359  yonedalem4b  15545  gsum2d2lem  17001  gsummptnn0fz  17014  gsummoncoe1  18346  elptr2  20075  ovoliunnul  21918  mbfinf  22072  itg2splitlem  22155  dgrle  22640  disjabrex  27443  disjabrexf  27444  disjunsn  27453  voliune  28201  volfiniune  28202  finminlem  30136  eq0rabdioph  30710  monotoddzz  30879  cncfiooicclem1  31696  stoweidlem28  31810  stoweidlem48  31830  stoweidlem58  31840  etransclem32  32049  bnj958  33998  bnj1491  34113  cdleme43fsv1snlem  36146  ltrniotaval  36307  cdlemksv2  36573  cdlemkuv2  36593  cdlemk36  36639  cdlemkid  36662  cdlemk19x  36669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-nfc 2607