Theorem nfel2 2930

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

Syntax hints:  Ⅎwnf 1856   ∈ wcel 2145  Ⅎwnfc 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902

This theorem is referenced by:  elabgt  3498  opelopabsb  5118  eliunxp  5398  opeliunxp2  5399  tz6.12f  6353  riotaxfrd  6785  0neqopab  6845  opeliunxp2f  7488  cbvixp  8079  boxcutc  8105  ixpiunwdom  8652  rankidb  8827  rankuni2b  8880  acni2  9069  ac6c4  9505  iundom2g  9564  tskuni  9807  reuccats1  13689  gsumcom2  18581  gsummatr01lem4  20683  ptclsg  21639  cnextfvval  22089  prdsdsf  22392  nnindf  29905  bnj1463  31461  ptrest  33741  sdclem1  33871  eqrelf  34363  binomcxplemnotnn0  39081  eliin2f  39808  stoweidlem26  40760  stoweidlem36  40770  stoweidlem46  40780  stoweidlem51  40785  eliunxp2  42640  setrec1  42966