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  5939  riota2f  5994  ovmpos  6145  ov2gf  6146  elovmporab  6222  elovmporab1w  6223  fmpox  6365  mpofvex  6370  qliftfuns  6788  xpf1o  7030  iunfidisj  7145  cc3  7487  infssuzcldc  10496  sumfct  11952  sumrbdclem  11956  summodclem3  11959  summodclem2a  11960  zsumdc  11963  fsumgcl  11965  fsum3  11966  isumss  11970  isumss2  11972  fsum3cvg2  11973  fsumsplitf  11987  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fisum0diag2  12026  fsummulc2  12027  fsum00  12041  fsumabs  12044  fsumrelem  12050  fsumiun  12056  isumshft  12069  mertenslem2  12115  prodrbdclem  12150  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  prodfct  12166  prodssdc  12168  fprodmul  12170  fprodm1s  12180  fprodp1s  12181  fprodcl2lem  12184  fprodabs  12195  fprod2dlemstep  12201  fprodcom2fi  12205  fprodrec  12208  fproddivapf  12210  fprodsplitf  12211  fprodsplit1f  12213  fprodle  12219  pcmpt  12934  pcmptdvds  12936  gsumfzfsumlemm  14620  iuncld  14858  fsumcncntop  15310  dvmptfsum  15468