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 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  eliunxp  5815  opeliunxp2  5816  tz6.12f  6915  riotaxfrd  7415  opeliunxp2f  8234  cbvixp  8949  boxcutc  8976  ixpiunwdom  9591  rankidb  9815  rankuni2b  9874  setrec1  9979  acni2  10132  ac6c4  10566  iundom2g  10631  tskuni  10875  reuccatpfxs1  14904  gsumcom2  20198  gsummatr01lem4  22982  ptclsg  23943  cnextfvval  24393  prdsdsf  24695  nnindf  33461  gsumpart  33674  nsgqusf1olem1  34014  nsgqusf1olem3  34016  bnj1463  35735  fineqvrep  35842  ptrest  38646  sdclem1  38786  eqrelf  39299  binomcxplemnotnn0  45449  eliin2f  46227  stoweidlem26  47144  stoweidlem36  47154  stoweidlem46  47164  stoweidlem51  47169  sge0f1o  47500  finfdm  47964  eliunxp2  49554