Theorem nfel2 2924

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892

This theorem is referenced by:  eliunxp  5848  opeliunxp2  5849  tz6.12f  6932  riotaxfrd  7422  opeliunxp2f  8235  cbvixp  8954  boxcutc  8981  ixpiunwdom  9630  rankidb  9840  rankuni2b  9893  acni2  10086  ac6c4  10521  iundom2g  10580  tskuni  10823  reuccatpfxs1  14785  gsumcom2  19993  gsummatr01lem4  22664  ptclsg  23623  cnextfvval  24073  prdsdsf  24377  nnindf  32821  gsumpart  33060  nsgqusf1olem1  33441  nsgqusf1olem3  33443  bnj1463  35069  fineqvrep  35109  ptrest  37626  sdclem1  37750  eqrelf  38256  binomcxplemnotnn0  44375  eliin2f  45109  stoweidlem26  46041  stoweidlem36  46051  stoweidlem46  46061  stoweidlem51  46066  sge0f1o  46397  finfdm  46861  eliunxp2  48250  setrec1  49210