Theorem nfel2 2628

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq2.1	|- F/_ x B

Assertion

Ref	Expression
nfel2	|- F/ x A e. B

Distinct variable group:   x, A

Allowed substitution hint:   B( x)

Proof of Theorem nfel2

Step	Hyp	Ref	Expression
1		nfcv 2612	. 2 |- F/_ x A
2		nfeq2.1	. 2 |- F/_ x B
3	1, 2	nfel 2624	1 |- F/ x A e. B

Syntax hints:   F/wnf 1675   e. wcel 1904   F/_wnfc 2599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601

This theorem is referenced by:  elabgt  3170  opelopabsb  4711  eliunxp  4977  opeliunxp2  4978  tz6.12f  5897  riotaxfrd  6300  0neqopab  6353  opeliunxp2f  6975  cbvixp  7557  boxcutc  7583  ixpiunwdom  8124  rankidb  8289  rankuni2b  8342  acni2  8495  ac6c4  8929  iundom2g  8983  tskuni  9226  gsumcom2  17685  gsummatr01lem4  19760  ptclsg  20707  cnextfvval  21158  prdsdsf  21460  nnindf  28457  bnj1463  29936  ptrest  32003  sdclem1  32136  binomcxplemnotnn0  36775  stoweidlem26  37998  stoweidlem36  38009  stoweidlem46  38019  stoweidlem51  38024  eliunxp2  40623