Theorem nfel1 2330

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

Hypothesis

Ref	Expression
nfeq1.1	|- F/_ x A

Assertion

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

Distinct variable group:   x, B

Allowed substitution hint:   A( x)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 |- F/_ x A
2		nfcv 2319	. 2 |- F/_ x B
3	1, 2	nfel 2328	1 |- F/ x A e. B

Syntax hints:   F/wnf 1460   e. wcel 2148   F/_wnfc 2306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308

This theorem is referenced by:  vtocl2gf  2799  vtocl3gf  2800  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  nfop  3794  pofun  4312  nfse  4341  rabxfrd  4469  mptfvex  5601  fvmptf  5608  fmptcof  5683  fliftfuns  5798  riota2f  5851  ovmpos  5997  ov2gf  5998  fmpox  6200  mpofvex  6203  qliftfuns  6618  xpf1o  6843  iunfidisj  6944  cc3  7266  sumfct  11381  sumrbdclem  11384  summodclem3  11387  summodclem2a  11388  zsumdc  11391  fsumgcl  11393  fsum3  11394  isumss  11398  isumss2  11400  fsum3cvg2  11401  fsumsplitf  11415  fsum2dlemstep  11441  fisumcom2  11445  fsumshftm  11452  fisum0diag2  11454  fsummulc2  11455  fsum00  11469  fsumabs  11472  fsumrelem  11478  fsumiun  11484  isumshft  11497  mertenslem2  11543  prodrbdclem  11578  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  prodfct  11594  prodssdc  11596  fprodmul  11598  fprodm1s  11608  fprodp1s  11609  fprodcl2lem  11612  fprodabs  11623  fprod2dlemstep  11629  fprodcom2fi  11633  fprodrec  11636  fproddivapf  11638  fprodsplitf  11639  fprodsplit1f  11641  fprodle  11647  infssuzcldc  11951  pcmpt  12340  pcmptdvds  12342  iuncld  13585  fsumcncntop  14026