Theorem nfel2 2911

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

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

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 2702

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 2722  df-clel 2804  df-nfc 2879

This theorem is referenced by:  eliunxp  5804  opeliunxp2  5805  tz6.12f  6887  riotaxfrd  7381  opeliunxp2f  8192  cbvixp  8890  boxcutc  8917  ixpiunwdom  9550  rankidb  9760  rankuni2b  9813  acni2  10006  ac6c4  10441  iundom2g  10500  tskuni  10743  reuccatpfxs1  14719  gsumcom2  19912  gsummatr01lem4  22552  ptclsg  23509  cnextfvval  23959  prdsdsf  24262  nnindf  32751  gsumpart  33004  nsgqusf1olem1  33391  nsgqusf1olem3  33393  bnj1463  35052  fineqvrep  35092  ptrest  37620  sdclem1  37744  eqrelf  38251  binomcxplemnotnn0  44352  eliin2f  45105  stoweidlem26  46031  stoweidlem36  46041  stoweidlem46  46051  stoweidlem51  46056  sge0f1o  46387  finfdm  46851  eliunxp2  48326  setrec1  49684