Theorem nfel2 2973

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  elabgt  3609  elabg  3614  opelopabsb  5382  0nelopab  5417  eliunxp  5672  opeliunxp2  5673  tz6.12f  6669  riotaxfrd  7127  opeliunxp2f  7859  cbvixp  8461  boxcutc  8488  ixpiunwdom  9038  rankidb  9213  rankuni2b  9266  acni2  9457  ac6c4  9892  iundom2g  9951  tskuni  10194  reuccatpfxs1  14100  gsumcom2  19088  gsummatr01lem4  21263  ptclsg  22220  cnextfvval  22670  prdsdsf  22974  nnindf  30561  gsumpart  30740  bnj1463  32437  ptrest  35056  sdclem1  35181  eqrelf  35677  binomcxplemnotnn0  41060  eliin2f  41740  stoweidlem26  42668  stoweidlem36  42678  stoweidlem46  42688  stoweidlem51  42693  eliunxp2  44735  setrec1  45221