Theorem nfel1 2386

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

Syntax hints:   F/wnf 1509   e. wcel 2202   F/_wnfc 2362

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364

This theorem is referenced by:  vtocl2gf  2867  vtocl3gf  2868  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  nfop  3883  pofun  4415  nfse  4444  rabxfrd  4572  mptfvex  5741  fvmptf  5748  fmptcof  5822  fliftfuns  5949  riota2f  6004  ovmpos  6155  ov2gf  6156  elovmporab  6232  elovmporab1w  6233  fmpox  6374  mpofvex  6379  qliftfuns  6831  xpf1o  7073  iunfidisj  7188  cc3  7547  infssuzcldc  10558  sumfct  12014  sumrbdclem  12018  summodclem3  12021  summodclem2a  12022  zsumdc  12025  fsumgcl  12027  fsum3  12028  isumss  12032  isumss2  12034  fsum3cvg2  12035  fsumsplitf  12049  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fisum0diag2  12088  fsummulc2  12089  fsum00  12103  fsumabs  12106  fsumrelem  12112  fsumiun  12118  isumshft  12131  mertenslem2  12177  prodrbdclem  12212  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  prodfct  12228  prodssdc  12230  fprodmul  12232  fprodm1s  12242  fprodp1s  12243  fprodcl2lem  12246  fprodabs  12257  fprod2dlemstep  12263  fprodcom2fi  12267  fprodrec  12270  fproddivapf  12272  fprodsplitf  12273  fprodsplit1f  12275  fprodle  12281  pcmpt  12996  pcmptdvds  12998  gsumfzfsumlemm  14683  iuncld  14926  fsumcncntop  15378  dvmptfsum  15536