Theorem nfel2 2917

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 2913	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2113  Ⅎwnfc 2879

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-cleq 2730  df-clel 2811  df-nfc 2881

This theorem is referenced by:  elabgt  3565  elabg  3570  0nelopab  5417  eliunxp  5674  opeliunxp2  5675  tz6.12f  6692  riotaxfrd  7156  opeliunxp2f  7898  cbvixp  8517  boxcutc  8544  ixpiunwdom  9120  rankidb  9295  rankuni2b  9348  acni2  9539  ac6c4  9974  iundom2g  10033  tskuni  10276  reuccatpfxs1  14191  gsumcom2  19207  gsummatr01lem4  21402  ptclsg  22359  cnextfvval  22809  prdsdsf  23113  nnindf  30700  gsumpart  30884  nsgqusf1olem1  31162  nsgqusf1olem3  31164  bnj1463  32598  fineqvrep  32627  ptrest  35388  sdclem1  35513  eqrelf  36007  binomcxplemnotnn0  41496  eliin2f  42176  stoweidlem26  43093  stoweidlem36  43103  stoweidlem46  43113  stoweidlem51  43118  eliunxp2  45187  setrec1  45834