Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel Unicode version

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
StepHypRef Expression
1 nfnfc.1 . . . 4
21a1i 11 . . 3
3 nfeq.2 . . . 4
43a1i 11 . . 3
52, 4nfeld 2627 . 2
65trud 1404 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator