Theorem nfel 2632

Description: Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-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
nfel

Proof of Theorem nfel

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	nfeld 2627	. 2
6	5	trud 1404	1

Syntax hints:  wtru 1396  F/wnf 1616  e.wcel 1818  F/_wnfc 2605

This theorem is referenced by:  nfel1  2635  nfel2  2637  nfnel  2800  elabgf  3244  elrabf  3255  sbcel12  3823  sbcel12gOLD  3824  rabxfrd  4673  ffnfvf  6058  mptelixpg  7526  ac6num  8880  ptcldmpt  20115  prdsdsf  20870  prdsxmet  20872  rmo4fOLD  27395  ssiun2sf  27427  funcnv4mpt  27512  ptrest  30048  aomclem8  31007  elunif  31391  rspcegf  31398  fsumsplit1  31573  fproddivf  31588  fprodsplit1f  31593  climsuse  31614  fprodcncf  31704  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem59  31841  fourierdlem31  31920  nfdfat  32215  bnj1491  34113

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-clel 2452  df-nfc 2607