Theorem nfel2 2945

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2146  Ⅎwnfc 2912

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2757  df-clel 2840  df-nfc 2914

This theorem is used by:  eliunxp  5825  opeliunxp2  5826  tz6.12f  6910  riotaxfrd  7410  opeliunxp2f  8212  cbvixp  8918  boxcutc  8945  ixpiunwdom  9559  rankidb  9779  rankuni2b  9832  acni2  10046  ac6c4  10480  iundom2g  10539  tskuni  10783  reuccatpfxs1  14806  gsumcom2  20089  gsummatr01lem4  22865  ptclsg  23823  cnextfvval  24273  prdsdsf  24575  nnindf  33234  gsumpart  33447  nsgqusf1olem1  33786  nsgqusf1olem3  33788  bnj1463  35508  fineqvrep  35584  ptrest  38327  sdclem1  38452  eqrelf  38965  binomcxplemnotnn0  45124  eliin2f  45880  stoweidlem26  46798  stoweidlem36  46808  stoweidlem46  46818  stoweidlem51  46823  sge0f1o  47154  finfdm  47618  eliunxp2  49171  setrec1  50526