Theorem nfel2 2910

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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2906	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

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 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  eliunxp  5801  opeliunxp2  5802  tz6.12f  6884  riotaxfrd  7378  opeliunxp2f  8189  cbvixp  8887  boxcutc  8914  ixpiunwdom  9543  rankidb  9753  rankuni2b  9806  acni2  9999  ac6c4  10434  iundom2g  10493  tskuni  10736  reuccatpfxs1  14712  gsumcom2  19905  gsummatr01lem4  22545  ptclsg  23502  cnextfvval  23952  prdsdsf  24255  nnindf  32744  gsumpart  32997  nsgqusf1olem1  33384  nsgqusf1olem3  33386  bnj1463  35045  fineqvrep  35085  ptrest  37613  sdclem1  37737  eqrelf  38244  binomcxplemnotnn0  44345  eliin2f  45098  stoweidlem26  46024  stoweidlem36  46034  stoweidlem46  46044  stoweidlem51  46049  sge0f1o  46380  finfdm  46844  eliunxp2  48322  setrec1  49680