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

Theorem nfel2 2767
 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:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfel2
StepHypRef Expression
1 nfcv 2751 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2763 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740 This theorem is referenced by:  elabgt  3316  opelopabsb  4910  eliunxp  5181  opeliunxp2  5182  tz6.12f  6122  riotaxfrd  6541  0neqopab  6596  opeliunxp2f  7223  cbvixp  7811  boxcutc  7837  ixpiunwdom  8379  rankidb  8546  rankuni2b  8599  acni2  8752  ac6c4  9186  iundom2g  9241  tskuni  9484  gsumcom2  18197  gsummatr01lem4  20283  ptclsg  21228  cnextfvval  21679  prdsdsf  21982  nnindf  28952  bnj1463  30377  ptrest  32578  sdclem1  32709  binomcxplemnotnn0  37577  stoweidlem26  38919  stoweidlem36  38929  stoweidlem46  38939  stoweidlem51  38944  eliunxp2  41905  setrec1  42237
 Copyright terms: Public domain W3C validator