Theorem nfel2 2940

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  eliunxp  5817  opeliunxp2  5818  tz6.12f  6903  riotaxfrd  7404  opeliunxp2f  8208  cbvixp  8921  boxcutc  8948  ixpiunwdom  9562  rankidb  9782  rankuni2b  9835  acni2  10049  ac6c4  10483  iundom2g  10548  tskuni  10792  reuccatpfxs1  14816  gsumcom2  20102  gsummatr01lem4  22880  ptclsg  23841  cnextfvval  24291  prdsdsf  24593  nnindf  33290  gsumpart  33503  nsgqusf1olem1  33842  nsgqusf1olem3  33844  bnj1463  35564  fineqvrep  35640  ptrest  38368  sdclem1  38493  eqrelf  39006  binomcxplemnotnn0  45180  eliin2f  45936  stoweidlem26  46854  stoweidlem36  46864  stoweidlem46  46874  stoweidlem51  46879  sge0f1o  47210  finfdm  47674  eliunxp2  49264  setrec1  50617