Theorem nfel1 2397

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

Syntax hints:   F/wnf 1509   e. wcel 2205   F/_wnfc 2373

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375

This theorem is referenced by:  vtocl2gf  2879  vtocl3gf  2880  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  nfop  3904  pofun  4438  nfse  4467  rabxfrd  4595  mptfvex  5768  fvmptf  5775  fmptcof  5849  fliftfuns  5977  riota2f  6034  ovmpos  6185  ov2gf  6186  elovmporab  6262  elovmporab1w  6263  fmpox  6409  mpofvex  6414  qliftfuns  6866  xpf1o  7110  iunfidisj  7226  cc3  7598  infssuzcldc  10617  sumfct  12084  sumrbdclem  12088  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsumsplitf  12119  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fisum0diag2  12158  fsummulc2  12159  fsum00  12173  fsumabs  12176  fsumrelem  12182  fsumiun  12188  isumshft  12201  mertenslem2  12247  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  prodfct  12298  prodssdc  12300  fprodmul  12302  fprodm1s  12312  fprodp1s  12313  fprodcl2lem  12316  fprodabs  12327  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  fprodle  12351  pcmpt  13066  pcmptdvds  13068  gsumfzfsumlemm  14861  iuncld  15106  fsumcncntop  15558  dvmptfsum  15716