Theorem nfel2 2630

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

Syntax hints:   F/wnf 1590   e. wcel 1758   F/_wnfc 2599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2443  df-clel 2446  df-nfc 2601

This theorem is referenced by:  elabgt  3200  opelopabsb  4697  eliunxp  5075  opeliunxp2  5076  tz6.12f  5807  riotaxfrd  6182  0neqopab  6230  cbvixp  7380  boxcutc  7406  ixpiunwdom  7907  rankidb  8108  rankuni2b  8161  acni2  8317  ac6c4  8751  iundom2g  8805  tskuni  9051  nfsum1  13269  nfsum  13270  gsumcom2  16572  gsummatr01lem4  18580  ptclsg  19304  cnextfvval  19753  prdsdsf  20058  ptrest  28563  mbfposadd  28577  sdclem1  28777  stoweidlem26  29959  stoweidlem36  29969  stoweidlem46  29979  stoweidlem51  29984  eliunxp2  30859  bnj1463  32346  bj-nfcf  32727