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  5780  opeliunxp2  5781  tz6.12f  6847  riotaxfrd  7340  opeliunxp2f  8143  cbvixp  8841  boxcutc  8868  ixpiunwdom  9482  rankidb  9696  rankuni2b  9749  acni2  9940  ac6c4  10375  iundom2g  10434  tskuni  10677  reuccatpfxs1  14653  gsumcom2  19854  gsummatr01lem4  22543  ptclsg  23500  cnextfvval  23950  prdsdsf  24253  nnindf  32764  gsumpart  33010  nsgqusf1olem1  33350  nsgqusf1olem3  33352  bnj1463  35022  fineqvrep  35070  ptrest  37599  sdclem1  37723  eqrelf  38230  binomcxplemnotnn0  44329  eliin2f  45082  stoweidlem26  46007  stoweidlem36  46017  stoweidlem46  46027  stoweidlem51  46032  sge0f1o  46363  finfdm  46827  eliunxp2  48318  setrec1  49676