Theorem nfeq 2627

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 2623	. 2
6	5	trud 1379	1

Syntax hints:  =wceq 1370  wtru 1371  F/wnf 1590  F/_wnfc 2602

This theorem is referenced by:  nfelOLD  2630  nfeq1  2631  nfeq2  2633  nfne  2784  raleqf  3022  rexeqf  3023  reueq1f  3024  rmoeq1f  3025  rabeqf  3074  csbhypf  3420  sbceqg  3791  nffn  5626  nffo  5741  fvmptdf  5908  mpteqb  5911  fvmptf  5913  eqfnfv2f  5924  dff13f  6098  ovmpt2s  6347  ov2gf  6348  ovmpt2dxf  6349  ovmpt2df  6355  eqerlem  7267  seqof2  12021  sumeq2w  13327  sumeq2ii  13328  sumss  13359  fsumadd  13373  fsummulc2  13409  fsumrelem  13428  txcnp  19592  ptcnplem  19593  cnmpt11  19635  cnmpt21  19643  cnmptcom  19650  mbfeqalem  21520  mbflim  21546  itgeq1f  21649  itgeqa  21691  dvmptfsum  21847  ulmss  22262  leibpi  22737  o1cxp  22768  lgseisenlem2  23089  istrkg2ld  23322  disjunsn  26404  opabdm  26411  opabrn  26412  mpt2mptxf  26462  f1od2  26491  fpwrelmap  26500  oms0  27166  prodeq1f  27877  prodeq2w  27881  prodeq2ii  27882  fprodmul  27927  fproddiv  27928  subtr  28969  subtr2  28970  iuneq2f  29427  mpt2bi123f  29435  mptbi12f  29439  dvdsrabdioph  29608  fphpd  29615  fvelrnbf  30200  refsum2cnlem1  30219  fmuldfeq  30362  climmulf  30375  climexp  30376  climsuse  30379  climrecf  30380  climaddf  30386  mullimc  30387  climf  30393  neglimc  30418  addlimc  30419  0ellimcdiv  30420  cncficcgt0  30456  cncfiooicclem1  30461  stoweidlem18  30547  stoweidlem31  30560  stoweidlem55  30584  stoweidlem59  30588  fourierdlem80  30716  ovmpt2rdxf  31603  bnj1316  32657  bnj1446  32879  bnj1447  32880  bnj1448  32881  bnj1519  32899  bnj1520  32900  bnj1529  32904  bj-sbeqALT  33247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2446  df-nfc 2604