Theorem nfel2 2918

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  eliunxp  5796  opeliunxp2  5797  tz6.12f  6869  riotaxfrd  7361  opeliunxp2f  8164  cbvixp  8866  boxcutc  8893  ixpiunwdom  9509  rankidb  9726  rankuni2b  9779  acni2  9970  ac6c4  10405  iundom2g  10464  tskuni  10708  reuccatpfxs1  14684  gsumcom2  19921  gsummatr01lem4  22619  ptclsg  23576  cnextfvval  24026  prdsdsf  24328  nnindf  32917  gsumpart  33163  nsgqusf1olem1  33512  nsgqusf1olem3  33514  bnj1463  35237  fineqvrep  35298  ptrest  37899  sdclem1  38023  eqrelf  38538  binomcxplemnotnn0  44741  eliin2f  45492  stoweidlem26  46413  stoweidlem36  46423  stoweidlem46  46433  stoweidlem51  46438  sge0f1o  46769  finfdm  47233  eliunxp2  48723  setrec1  50079