Theorem nfel1 2403

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

Syntax hints:   F/wnf 1513   e. wcel 2209   F/_wnfc 2379

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381

This theorem is referenced by:  vtocl2gf  2885  vtocl3gf  2886  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  nfop  3915  pofun  4452  nfse  4481  rabxfrd  4610  mptfvex  5785  fvmptf  5792  fmptcof  5866  fliftfuns  5994  riota2f  6051  ovmpos  6202  ov2gf  6203  elovmporab  6279  elovmporab1w  6280  fmpox  6426  mpofvex  6431  qliftfuns  6883  xpf1o  7134  iunfidisj  7250  cc3  7624  infssuzcldc  10646  sumfct  12118  sumrbdclem  12122  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsumsplitf  12153  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fisum0diag2  12192  fsummulc2  12193  fsum00  12207  fsumabs  12210  fsumrelem  12216  fsumiun  12222  isumshft  12235  mertenslem2  12281  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  prodfct  12332  prodssdc  12334  fprodmul  12336  fprodm1s  12346  fprodp1s  12347  fprodcl2lem  12350  fprodabs  12361  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  fprodle  12385  pcmpt  13100  pcmptdvds  13102  gsummptfidmadd  14138  iuncld  15139  fsumcncntop  15591  dvmptfsum  15749