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  5786  opeliunxp2  5787  tz6.12f  6859  riotaxfrd  7351  opeliunxp2f  8153  cbvixp  8855  boxcutc  8882  ixpiunwdom  9498  rankidb  9715  rankuni2b  9768  acni2  9959  ac6c4  10394  iundom2g  10453  tskuni  10697  reuccatpfxs1  14700  gsumcom2  19941  gsummatr01lem4  22633  ptclsg  23590  cnextfvval  24040  prdsdsf  24342  nnindf  32908  gsumpart  33139  nsgqusf1olem1  33488  nsgqusf1olem3  33490  bnj1463  35213  fineqvrep  35274  ptrest  37954  sdclem1  38078  eqrelf  38593  binomcxplemnotnn0  44801  eliin2f  45552  stoweidlem26  46472  stoweidlem36  46482  stoweidlem46  46492  stoweidlem51  46497  sge0f1o  46828  finfdm  47292  eliunxp2  48822  setrec1  50178