Theorem nfel2 2921

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

Syntax hints:  Ⅎwnf 1779   ∈ wcel 2105  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-clel 2813  df-nfc 2889

This theorem is referenced by:  elabgtOLDOLD  3673  elabgOLD  3677  eliunxp  5850  opeliunxp2  5851  tz6.12f  6932  riotaxfrd  7421  opeliunxp2f  8233  cbvixp  8952  boxcutc  8979  ixpiunwdom  9627  rankidb  9837  rankuni2b  9890  acni2  10083  ac6c4  10518  iundom2g  10577  tskuni  10820  reuccatpfxs1  14781  gsumcom2  20007  gsummatr01lem4  22679  ptclsg  23638  cnextfvval  24088  prdsdsf  24392  nnindf  32825  gsumpart  33042  nsgqusf1olem1  33420  nsgqusf1olem3  33422  bnj1463  35047  fineqvrep  35087  ptrest  37605  sdclem1  37729  eqrelf  38236  binomcxplemnotnn0  44351  eliin2f  45043  stoweidlem26  45981  stoweidlem36  45991  stoweidlem46  46001  stoweidlem51  46006  sge0f1o  46337  finfdm  46801  eliunxp2  48178  setrec1  48921