Theorem nfel2 2781

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

Syntax hints:  Ⅎwnf 1708   ∈ wcel 1990  Ⅎwnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  elabgt  3347  opelopabsb  4985  eliunxp  5259  opeliunxp2  5260  tz6.12f  6212  riotaxfrd  6642  0neqopab  6698  opeliunxp2f  7336  cbvixp  7925  boxcutc  7951  ixpiunwdom  8496  rankidb  8663  rankuni2b  8716  acni2  8869  ac6c4  9303  iundom2g  9362  tskuni  9605  reuccats1  13480  gsumcom2  18374  gsummatr01lem4  20464  ptclsg  21418  cnextfvval  21869  prdsdsf  22172  nnindf  29565  bnj1463  31123  ptrest  33408  sdclem1  33539  eqrelf  34020  binomcxplemnotnn0  38555  eliin2f  39287  stoweidlem26  40243  stoweidlem36  40253  stoweidlem46  40263  stoweidlem51  40268  eliunxp2  42112  setrec1  42438