Theorem nfel2 2913

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2806  df-nfc 2881

This theorem is referenced by:  eliunxp  5772  opeliunxp2  5773  tz6.12f  6842  riotaxfrd  7332  opeliunxp2f  8135  cbvixp  8833  boxcutc  8860  ixpiunwdom  9471  rankidb  9688  rankuni2b  9741  acni2  9932  ac6c4  10367  iundom2g  10426  tskuni  10669  reuccatpfxs1  14649  gsumcom2  19882  gsummatr01lem4  22568  ptclsg  23525  cnextfvval  23975  prdsdsf  24277  nnindf  32794  gsumpart  33029  nsgqusf1olem1  33370  nsgqusf1olem3  33372  bnj1463  35059  fineqvrep  35129  ptrest  37659  sdclem1  37783  eqrelf  38290  binomcxplemnotnn0  44389  eliin2f  45141  stoweidlem26  46064  stoweidlem36  46074  stoweidlem46  46084  stoweidlem51  46089  sge0f1o  46420  finfdm  46884  eliunxp2  48365  setrec1  49723