Theorem nfel1 2359

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

Syntax hints:   F/wnf 1483   e. wcel 2176   F/_wnfc 2335

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  vtocl2gf  2835  vtocl3gf  2836  vtoclgaf  2838  vtocl2gaf  2840  vtocl3gaf  2842  nfop  3835  pofun  4360  nfse  4389  rabxfrd  4517  mptfvex  5667  fvmptf  5674  fmptcof  5749  fliftfuns  5869  riota2f  5923  ovmpos  6071  ov2gf  6072  elovmporab  6148  elovmporab1w  6149  fmpox  6288  mpofvex  6293  qliftfuns  6708  xpf1o  6943  iunfidisj  7050  cc3  7382  infssuzcldc  10380  sumfct  11718  sumrbdclem  11721  summodclem3  11724  summodclem2a  11725  zsumdc  11728  fsumgcl  11730  fsum3  11731  isumss  11735  isumss2  11737  fsum3cvg2  11738  fsumsplitf  11752  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fisum0diag2  11791  fsummulc2  11792  fsum00  11806  fsumabs  11809  fsumrelem  11815  fsumiun  11821  isumshft  11834  mertenslem2  11880  prodrbdclem  11915  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  prodfct  11931  prodssdc  11933  fprodmul  11935  fprodm1s  11945  fprodp1s  11946  fprodcl2lem  11949  fprodabs  11960  fprod2dlemstep  11966  fprodcom2fi  11970  fprodrec  11973  fproddivapf  11975  fprodsplitf  11976  fprodsplit1f  11978  fprodle  11984  pcmpt  12699  pcmptdvds  12701  gsumfzfsumlemm  14382  iuncld  14620  fsumcncntop  15072  dvmptfsum  15230