Theorem nfel2 2582

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 2564	. 2 |- F/_ x A
2		nfeq2.1	. 2 |- F/_ x B
3	1, 2	nfel 2577	1 |- F/ x A e. B

Syntax hints:   F/wnf 1637   e. wcel 1842   F/_wnfc 2550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-cleq 2394  df-clel 2397  df-nfc 2552

This theorem is referenced by:  elabgt  3192  opelopabsb  4699  eliunxp  5082  opeliunxp2  5083  tz6.12f  5823  riotaxfrd  6226  0neqopab  6278  cbvixp  7444  boxcutc  7470  ixpiunwdom  7971  rankidb  8170  rankuni2b  8223  acni2  8379  ac6c4  8813  iundom2g  8867  tskuni  9111  gsumcom2  17216  gsummatr01lem4  19344  ptclsg  20300  cnextfvval  20749  prdsdsf  21054  nnindf  27941  bnj1463  29319  ptrest  31401  sdclem1  31499  binomcxplemnotnn0  36090  stoweidlem26  37158  stoweidlem36  37168  stoweidlem46  37178  stoweidlem51  37183  eliunxp2  38414