Theorem nfel1 2350

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfel1	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2339	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2348	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1474   ∈ wcel 2167  Ⅎ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  3824  pofun  4347  nfse  4376  rabxfrd  4504  mptfvex  5647  fvmptf  5654  fmptcof  5729  fliftfuns  5845  riota2f  5899  ovmpos  6046  ov2gf  6047  elovmporab  6123  elovmporab1w  6124  fmpox  6258  mpofvex  6263  qliftfuns  6678  xpf1o  6905  iunfidisj  7012  cc3  7335  infssuzcldc  10325  sumfct  11539  sumrbdclem  11542  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsumsplitf  11573  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fisum0diag2  11612  fsummulc2  11613  fsum00  11627  fsumabs  11630  fsumrelem  11636  fsumiun  11642  isumshft  11655  mertenslem2  11701  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  prodfct  11752  prodssdc  11754  fprodmul  11756  fprodm1s  11766  fprodp1s  11767  fprodcl2lem  11770  fprodabs  11781  fprod2dlemstep  11787  fprodcom2fi  11791  fprodrec  11794  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  fprodle  11805  pcmpt  12512  pcmptdvds  12514  gsumfzfsumlemm  14143  iuncld  14351  fsumcncntop  14803  dvmptfsum  14961