Theorem nfel1 2395

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

Syntax hints:   F/wnf 1509   e. wcel 2203   F/_wnfc 2371

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373

This theorem is referenced by:  vtocl2gf  2876  vtocl3gf  2877  vtoclgaf  2879  vtocl2gaf  2881  vtocl3gaf  2883  nfop  3898  pofun  4432  nfse  4461  rabxfrd  4589  mptfvex  5762  fvmptf  5769  fmptcof  5843  fliftfuns  5970  riota2f  6025  ovmpos  6176  ov2gf  6177  elovmporab  6253  elovmporab1w  6254  fmpox  6395  mpofvex  6400  qliftfuns  6852  xpf1o  7096  iunfidisj  7212  cc3  7581  infssuzcldc  10594  sumfct  12055  sumrbdclem  12059  summodclem3  12062  summodclem2a  12063  zsumdc  12066  fsumgcl  12068  fsum3  12069  isumss  12073  isumss2  12075  fsum3cvg2  12076  fsumsplitf  12090  fsum2dlemstep  12116  fisumcom2  12120  fsumshftm  12127  fisum0diag2  12129  fsummulc2  12130  fsum00  12144  fsumabs  12147  fsumrelem  12153  fsumiun  12159  isumshft  12172  mertenslem2  12218  prodrbdclem  12253  prodmodclem3  12257  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  prodfct  12269  prodssdc  12271  fprodmul  12273  fprodm1s  12283  fprodp1s  12284  fprodcl2lem  12287  fprodabs  12298  fprod2dlemstep  12304  fprodcom2fi  12308  fprodrec  12311  fproddivapf  12313  fprodsplitf  12314  fprodsplit1f  12316  fprodle  12322  pcmpt  13037  pcmptdvds  13039  gsumfzfsumlemm  14727  iuncld  14972  fsumcncntop  15424  dvmptfsum  15582