Theorem nfel1 2385

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 2374	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2383	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1508   ∈ wcel 2202  Ⅎwnfc 2361

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363

This theorem is referenced by:  vtocl2gf  2866  vtocl3gf  2867  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  nfop  3878  pofun  4409  nfse  4438  rabxfrd  4566  mptfvex  5732  fvmptf  5739  fmptcof  5814  fliftfuns  5938  riota2f  5993  ovmpos  6144  ov2gf  6145  elovmporab  6221  elovmporab1w  6222  fmpox  6364  mpofvex  6369  qliftfuns  6787  xpf1o  7029  iunfidisj  7144  cc3  7486  infssuzcldc  10494  sumfct  11934  sumrbdclem  11937  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsumsplitf  11968  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fisum0diag2  12007  fsummulc2  12008  fsum00  12022  fsumabs  12025  fsumrelem  12031  fsumiun  12037  isumshft  12050  mertenslem2  12096  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  prodfct  12147  prodssdc  12149  fprodmul  12151  fprodm1s  12161  fprodp1s  12162  fprodcl2lem  12165  fprodabs  12176  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  fprodle  12200  pcmpt  12915  pcmptdvds  12917  gsumfzfsumlemm  14600  iuncld  14838  fsumcncntop  15290  dvmptfsum  15448