Theorem nfel2 2919

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

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2119  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-clel 2814  df-nfc 2888

This theorem is referenced by:  eliunxp  5779  opeliunxp2  5780  tz6.12f  6852  riotaxfrd  7347  opeliunxp2f  8150  cbvixp  8852  boxcutc  8879  ixpiunwdom  9495  rankidb  9715  rankuni2b  9768  acni2  9959  ac6c4  10394  iundom2g  10453  tskuni  10697  reuccatpfxs1  14700  gsumcom2  19941  gsummatr01lem4  22641  ptclsg  23598  cnextfvval  24048  prdsdsf  24350  nnindf  32912  gsumpart  33144  nsgqusf1olem1  33496  nsgqusf1olem3  33498  bnj1463  35237  fineqvrep  35295  ptrest  37986  sdclem1  38110  eqrelf  38625  binomcxplemnotnn0  44800  eliin2f  45551  stoweidlem26  46469  stoweidlem36  46479  stoweidlem46  46489  stoweidlem51  46494  sge0f1o  46825  finfdm  47289  eliunxp2  48825  setrec1  50181