Theorem nfel2 2810

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

Syntax hints:  Ⅎwnf 1748   ∈ wcel 2030  Ⅎwnfc 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782

This theorem is referenced by:  elabgt  3379  opelopabsb  5014  eliunxp  5292  opeliunxp2  5293  tz6.12f  6250  riotaxfrd  6682  0neqopab  6740  opeliunxp2f  7381  cbvixp  7967  boxcutc  7993  ixpiunwdom  8537  rankidb  8701  rankuni2b  8754  acni2  8907  ac6c4  9341  iundom2g  9400  tskuni  9643  reuccats1  13526  gsumcom2  18420  gsummatr01lem4  20512  ptclsg  21466  cnextfvval  21916  prdsdsf  22219  nnindf  29693  bnj1463  31249  ptrest  33538  sdclem1  33669  eqrelf  34161  binomcxplemnotnn0  38872  eliin2f  39601  stoweidlem26  40561  stoweidlem36  40571  stoweidlem46  40581  stoweidlem51  40586  eliunxp2  42437  setrec1  42763