Theorem nfel1 2383

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

Syntax hints:   F/wnf 1506   e. wcel 2200   F/_wnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  vtocl2gf  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  nfop  3873  pofun  4403  nfse  4432  rabxfrd  4560  mptfvex  5720  fvmptf  5727  fmptcof  5802  fliftfuns  5922  riota2f  5977  ovmpos  6128  ov2gf  6129  elovmporab  6205  elovmporab1w  6206  fmpox  6346  mpofvex  6351  qliftfuns  6766  xpf1o  7005  iunfidisj  7113  cc3  7454  infssuzcldc  10455  sumfct  11885  sumrbdclem  11888  summodclem3  11891  summodclem2a  11892  zsumdc  11895  fsumgcl  11897  fsum3  11898  isumss  11902  isumss2  11904  fsum3cvg2  11905  fsumsplitf  11919  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fisum0diag2  11958  fsummulc2  11959  fsum00  11973  fsumabs  11976  fsumrelem  11982  fsumiun  11988  isumshft  12001  mertenslem2  12047  prodrbdclem  12082  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  prodfct  12098  prodssdc  12100  fprodmul  12102  fprodm1s  12112  fprodp1s  12113  fprodcl2lem  12116  fprodabs  12127  fprod2dlemstep  12133  fprodcom2fi  12137  fprodrec  12140  fproddivapf  12142  fprodsplitf  12143  fprodsplit1f  12145  fprodle  12151  pcmpt  12866  pcmptdvds  12868  gsumfzfsumlemm  14551  iuncld  14789  fsumcncntop  15241  dvmptfsum  15399