Theorem nfel2 2767

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

Syntax hints:  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740

This theorem is referenced by:  elabgt  3316  opelopabsb  4910  eliunxp  5181  opeliunxp2  5182  tz6.12f  6122  riotaxfrd  6541  0neqopab  6596  opeliunxp2f  7223  cbvixp  7811  boxcutc  7837  ixpiunwdom  8379  rankidb  8546  rankuni2b  8599  acni2  8752  ac6c4  9186  iundom2g  9241  tskuni  9484  gsumcom2  18197  gsummatr01lem4  20283  ptclsg  21228  cnextfvval  21679  prdsdsf  21982  nnindf  28952  bnj1463  30377  ptrest  32578  sdclem1  32709  binomcxplemnotnn0  37577  stoweidlem26  38919  stoweidlem36  38929  stoweidlem46  38939  stoweidlem51  38944  eliunxp2  41905  setrec1  42237