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

Syntax hints:  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-clel 2817  df-nfc 2888

This theorem is referenced by:  elabgtOLD  3597  elabgOLD  3601  0nelopabOLD  5472  eliunxp  5735  opeliunxp2  5736  tz6.12f  6780  riotaxfrd  7247  opeliunxp2f  7997  cbvixp  8660  boxcutc  8687  ixpiunwdom  9279  rankidb  9489  rankuni2b  9542  acni2  9733  ac6c4  10168  iundom2g  10227  tskuni  10470  reuccatpfxs1  14388  gsumcom2  19491  gsummatr01lem4  21715  ptclsg  22674  cnextfvval  23124  prdsdsf  23428  nnindf  31035  gsumpart  31217  nsgqusf1olem1  31500  nsgqusf1olem3  31502  bnj1463  32935  fineqvrep  32964  ptrest  35703  sdclem1  35828  eqrelf  36322  binomcxplemnotnn0  41863  eliin2f  42543  stoweidlem26  43457  stoweidlem36  43467  stoweidlem46  43477  stoweidlem51  43482  eliunxp2  45557  setrec1  46283