Theorem nfel1 2350

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

Syntax hints:   F/wnf 1474   e. wcel 2167   F/_wnfc 2326

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  vtocl2gf  2826  vtocl3gf  2827  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  nfop  3825  pofun  4348  nfse  4377  rabxfrd  4505  mptfvex  5648  fvmptf  5655  fmptcof  5730  fliftfuns  5846  riota2f  5900  ovmpos  6048  ov2gf  6049  elovmporab  6125  elovmporab1w  6126  fmpox  6260  mpofvex  6265  qliftfuns  6680  xpf1o  6907  iunfidisj  7014  cc3  7338  infssuzcldc  10328  sumfct  11542  sumrbdclem  11545  summodclem3  11548  summodclem2a  11549  zsumdc  11552  fsumgcl  11554  fsum3  11555  isumss  11559  isumss2  11561  fsum3cvg2  11562  fsumsplitf  11576  fsum2dlemstep  11602  fisumcom2  11606  fsumshftm  11613  fisum0diag2  11615  fsummulc2  11616  fsum00  11630  fsumabs  11633  fsumrelem  11639  fsumiun  11645  isumshft  11658  mertenslem2  11704  prodrbdclem  11739  prodmodclem3  11743  prodmodclem2a  11744  zproddc  11747  fprodseq  11751  prodfct  11755  prodssdc  11757  fprodmul  11759  fprodm1s  11769  fprodp1s  11770  fprodcl2lem  11773  fprodabs  11784  fprod2dlemstep  11790  fprodcom2fi  11794  fprodrec  11797  fproddivapf  11799  fprodsplitf  11800  fprodsplit1f  11802  fprodle  11808  pcmpt  12523  pcmptdvds  12525  gsumfzfsumlemm  14169  iuncld  14377  fsumcncntop  14829  dvmptfsum  14987