Theorem nfel2 2944

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2755  df-clel 2839  df-nfc 2913

This theorem is used by:  eliunxp  5824  opeliunxp2  5825  tz6.12f  6941  riotaxfrd  7442  opeliunxp2f  8265  cbvixp  8980  boxcutc  9007  ixpiunwdom  9621  rankidb  9845  rankuni2b  9904  setrec1  10009  acni2  10164  ac6c4  10598  iundom2g  10663  tskuni  10907  reuccatpfxs1  14938  gsumcom2  20240  gsummatr01lem4  23028  ptclsg  23989  cnextfvval  24439  prdsdsf  24741  nnindf  33507  gsumpart  33723  nsgqusf1olem1  34068  nsgqusf1olem3  34070  bnj1463  35796  fineqvrep  35923  ptrest  38805  sdclem1  38943  eqrelf  39456  binomcxplemnotnn0  45601  eliin2f  46392  stoweidlem26  47309  stoweidlem36  47319  stoweidlem46  47329  stoweidlem51  47334  sge0f1o  47665  finfdm  48129  eliunxp2  49777