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

Theorem nfel2 2637
 Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1
Assertion
Ref Expression
nfel2
Distinct variable group:   ,

Proof of Theorem nfel2
StepHypRef Expression
1 nfcv 2619 . 2
2 nfeq2.1 . 2
31, 2nfel 2632 1
 Colors of variables: wff setvar class Syntax hints:  F/wnf 1616  e.wcel 1818  F/_wnfc 2605 This theorem is referenced by:  elabgt  3243  opelopabsb  4762  eliunxp  5145  opeliunxp2  5146  tz6.12f  5889  riotaxfrd  6288  0neqopab  6341  cbvixp  7506  boxcutc  7532  ixpiunwdom  8038  rankidb  8239  rankuni2b  8292  acni2  8448  ac6c4  8882  iundom2g  8936  tskuni  9182  gsumcom2  17003  gsummatr01lem4  19160  ptclsg  20116  cnextfvval  20565  prdsdsf  20870  nnindf  27610  ptrest  30048  sdclem1  30236  binomcxplemnotnn0  31261  stoweidlem26  31808  stoweidlem36  31818  stoweidlem46  31828  stoweidlem51  31833  eliunxp2  32923  bnj1463  34111 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