Theorem nfeq 2630

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypotheses

Ref	Expression
nfnfc.1
nfeq.2

Assertion

Ref	Expression
nfeq

Proof of Theorem nfeq

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4
2	1	a1i 11	. . 3
3		nfeq.2	. . . 4
4	3	a1i 11	. . 3
5	2, 4	nfeqd 2626	. 2
6	5	trud 1404	1

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

This theorem is referenced by:  nfelOLD  2633  nfeq1  2634  nfeq2  2636  nfne  2788  raleqf  3050  rexeqf  3051  reueq1f  3052  rmoeq1f  3053  rabeqf  3102  csbhypf  3453  sbceqg  3825  nffn  5682  nffo  5799  fvmptdf  5967  mpteqb  5970  fvmptf  5972  eqfnfv2f  5985  dff13f  6167  ovmpt2s  6426  ov2gf  6427  ovmpt2dxf  6428  ovmpt2df  6434  eqerlem  7362  seqof2  12165  sumeq2ii  13515  sumss  13546  fsumadd  13561  fsummulc2  13599  fsumrelem  13621  prodeq1f  13715  prodeq2ii  13720  fprodmul  13765  fproddiv  13766  txcnp  20121  ptcnplem  20122  cnmpt11  20164  cnmpt21  20172  cnmptcom  20179  mbfeqalem  22049  mbflim  22075  itgeq1f  22178  itgeqa  22220  dvmptfsum  22376  ulmss  22792  leibpi  23273  o1cxp  23304  lgseisenlem2  23625  subtr  30132  subtr2  30133  iuneq2f  30563  mpt2bi123f  30571  mptbi12f  30575  dvdsrabdioph  30743  fphpd  30750  fvelrnbf  31393  refsum2cnlem1  31412  fmuldfeq  31577  fprodle  31604  mccl  31606  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climaddf  31621  mullimc  31622  neglimc  31653  addlimc  31654  0ellimcdiv  31655  dvnmptdivc  31735  dvmptfprod  31742  dvnprodlem1  31743  stoweidlem18  31800  stoweidlem31  31813  stoweidlem55  31837  stoweidlem59  31841  ovmpt2rdxf  32928  bnj1316  33879  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1519  34121  bnj1520  34122  bnj1529  34126  bj-sbeqALT  34467

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