Theorem nfel2 2950

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

Syntax hints:  Ⅎwnf 1827   ∈ wcel 2107  Ⅎwnfc 2919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2770  df-clel 2774  df-nfc 2921

This theorem is referenced by:  elabgt  3553  elabg  3556  opelopabsb  5222  eliunxp  5505  opeliunxp2  5506  tz6.12f  6470  riotaxfrd  6914  0neqopab  6975  opeliunxp2f  7618  cbvixp  8211  boxcutc  8237  ixpiunwdom  8785  rankidb  8960  rankuni2b  9013  acni2  9202  ac6c4  9638  iundom2g  9697  tskuni  9940  reuccats1OLD  13848  reuccatpfxs1  13883  gsumcom2  18760  gsummatr01lem4  20870  ptclsg  21827  cnextfvval  22277  prdsdsf  22580  nnindf  30129  bnj1463  31722  ptrest  34034  sdclem1  34163  eqrelf  34655  binomcxplemnotnn0  39511  eliin2f  40216  stoweidlem26  41170  stoweidlem36  41180  stoweidlem46  41190  stoweidlem51  41195  eliunxp2  43127  setrec1  43543