Theorem nfel2 2917

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

Step	Hyp	Ref	Expression
1		nfcv 2898	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2913	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2727  df-clel 2809  df-nfc 2885

This theorem is referenced by:  eliunxp  5817  opeliunxp2  5818  tz6.12f  6902  riotaxfrd  7396  opeliunxp2f  8209  cbvixp  8928  boxcutc  8955  ixpiunwdom  9604  rankidb  9814  rankuni2b  9867  acni2  10060  ac6c4  10495  iundom2g  10554  tskuni  10797  reuccatpfxs1  14765  gsumcom2  19956  gsummatr01lem4  22596  ptclsg  23553  cnextfvval  24003  prdsdsf  24306  nnindf  32798  gsumpart  33051  nsgqusf1olem1  33428  nsgqusf1olem3  33430  bnj1463  35086  fineqvrep  35126  ptrest  37643  sdclem1  37767  eqrelf  38273  binomcxplemnotnn0  44380  eliin2f  45128  stoweidlem26  46055  stoweidlem36  46065  stoweidlem46  46075  stoweidlem51  46080  sge0f1o  46411  finfdm  46875  eliunxp2  48309  setrec1  49555