Theorem nfel2 2642

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

Syntax hints:   F/wnf 1594   e. wcel 1762   F/_wnfc 2610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612

This theorem is referenced by:  elabgt  3242  opelopabsb  4752  eliunxp  5133  opeliunxp2  5134  tz6.12f  5877  riotaxfrd  6269  0neqopab  6318  cbvixp  7478  boxcutc  7504  ixpiunwdom  8008  rankidb  8209  rankuni2b  8262  acni2  8418  ac6c4  8852  iundom2g  8906  tskuni  9152  nfsum1  13463  nfsum  13464  gsumcom2  16789  gsummatr01lem4  18922  ptclsg  19846  cnextfvval  20295  prdsdsf  20600  ptrest  29614  mbfposadd  29628  sdclem1  29828  stoweidlem26  31283  stoweidlem36  31293  stoweidlem46  31303  stoweidlem51  31308  eliunxp2  31864  bnj1463  33067  bj-nfcf  33450