Theorem nfel2 2941

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

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

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 2733

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 2753  df-clel 2836  df-nfc 2910

This theorem is used by:  eliunxp  5814  opeliunxp2  5815  tz6.12f  6908  riotaxfrd  7409  opeliunxp2f  8220  cbvixp  8935  boxcutc  8962  ixpiunwdom  9577  rankidb  9801  rankuni2b  9860  setrec1  9965  acni2  10118  ac6c4  10552  iundom2g  10617  tskuni  10861  reuccatpfxs1  14889  gsumcom2  20182  gsummatr01lem4  22966  ptclsg  23927  cnextfvval  24377  prdsdsf  24679  nnindf  33404  gsumpart  33617  nsgqusf1olem1  33957  nsgqusf1olem3  33959  bnj1463  35678  fineqvrep  35765  ptrest  38517  sdclem1  38657  eqrelf  39170  binomcxplemnotnn0  45325  eliin2f  46088  stoweidlem26  47005  stoweidlem36  47015  stoweidlem46  47025  stoweidlem51  47030  sge0f1o  47361  finfdm  47825  eliunxp2  49415