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

Theorem nfel2 2810
 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 2793 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2806 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1748   ∈ wcel 2030  Ⅎwnfc 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782 This theorem is referenced by:  elabgt  3379  opelopabsb  5014  eliunxp  5292  opeliunxp2  5293  tz6.12f  6250  riotaxfrd  6682  0neqopab  6740  opeliunxp2f  7381  cbvixp  7967  boxcutc  7993  ixpiunwdom  8537  rankidb  8701  rankuni2b  8754  acni2  8907  ac6c4  9341  iundom2g  9400  tskuni  9643  reuccats1  13526  gsumcom2  18420  gsummatr01lem4  20512  ptclsg  21466  cnextfvval  21916  prdsdsf  22219  nnindf  29693  bnj1463  31249  ptrest  33538  sdclem1  33669  eqrelf  34161  binomcxplemnotnn0  38872  eliin2f  39601  stoweidlem26  40561  stoweidlem36  40571  stoweidlem46  40581  stoweidlem51  40586  eliunxp2  42437  setrec1  42763
 Copyright terms: Public domain W3C validator