Theorem nfel1 2340

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

Syntax hints:   F/wnf 1470   e. wcel 2158   F/_wnfc 2316

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-cleq 2180  df-clel 2183  df-nfc 2318

This theorem is referenced by:  vtocl2gf  2811  vtocl3gf  2812  vtoclgaf  2814  vtocl2gaf  2816  vtocl3gaf  2818  nfop  3806  pofun  4324  nfse  4353  rabxfrd  4481  mptfvex  5614  fvmptf  5621  fmptcof  5696  fliftfuns  5812  riota2f  5865  ovmpos  6012  ov2gf  6013  fmpox  6215  mpofvex  6218  qliftfuns  6633  xpf1o  6858  iunfidisj  6959  cc3  7281  sumfct  11396  sumrbdclem  11399  summodclem3  11402  summodclem2a  11403  zsumdc  11406  fsumgcl  11408  fsum3  11409  isumss  11413  isumss2  11415  fsum3cvg2  11416  fsumsplitf  11430  fsum2dlemstep  11456  fisumcom2  11460  fsumshftm  11467  fisum0diag2  11469  fsummulc2  11470  fsum00  11484  fsumabs  11487  fsumrelem  11493  fsumiun  11499  isumshft  11512  mertenslem2  11558  prodrbdclem  11593  prodmodclem3  11597  prodmodclem2a  11598  zproddc  11601  fprodseq  11605  prodfct  11609  prodssdc  11611  fprodmul  11613  fprodm1s  11623  fprodp1s  11624  fprodcl2lem  11627  fprodabs  11638  fprod2dlemstep  11644  fprodcom2fi  11648  fprodrec  11651  fproddivapf  11653  fprodsplitf  11654  fprodsplit1f  11656  fprodle  11662  infssuzcldc  11966  pcmpt  12355  pcmptdvds  12357  iuncld  13911  fsumcncntop  14352