Theorem nfel1 2361

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

Syntax hints:   F/wnf 1484   e. wcel 2178   F/_wnfc 2337

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339

This theorem is referenced by:  vtocl2gf  2840  vtocl3gf  2841  vtoclgaf  2843  vtocl2gaf  2845  vtocl3gaf  2847  nfop  3849  pofun  4377  nfse  4406  rabxfrd  4534  mptfvex  5688  fvmptf  5695  fmptcof  5770  fliftfuns  5890  riota2f  5944  ovmpos  6092  ov2gf  6093  elovmporab  6169  elovmporab1w  6170  fmpox  6309  mpofvex  6314  qliftfuns  6729  xpf1o  6966  iunfidisj  7074  cc3  7415  infssuzcldc  10415  sumfct  11800  sumrbdclem  11803  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsumsplitf  11834  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fisum0diag2  11873  fsummulc2  11874  fsum00  11888  fsumabs  11891  fsumrelem  11897  fsumiun  11903  isumshft  11916  mertenslem2  11962  prodrbdclem  11997  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  prodfct  12013  prodssdc  12015  fprodmul  12017  fprodm1s  12027  fprodp1s  12028  fprodcl2lem  12031  fprodabs  12042  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  fprodle  12066  pcmpt  12781  pcmptdvds  12783  gsumfzfsumlemm  14464  iuncld  14702  fsumcncntop  15154  dvmptfsum  15312