Theorem nfel1 2386

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

Syntax hints:  Ⅎwnf 1509   ∈ wcel 2202  Ⅎwnfc 2362

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364

This theorem is referenced by:  vtocl2gf  2867  vtocl3gf  2868  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  nfop  3883  pofun  4415  nfse  4444  rabxfrd  4572  mptfvex  5741  fvmptf  5748  fmptcof  5822  fliftfuns  5949  riota2f  6004  ovmpos  6155  ov2gf  6156  elovmporab  6232  elovmporab1w  6233  fmpox  6374  mpofvex  6379  qliftfuns  6831  xpf1o  7073  iunfidisj  7188  cc3  7530  infssuzcldc  10541  sumfct  11997  sumrbdclem  12001  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsumsplitf  12032  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fisum0diag2  12071  fsummulc2  12072  fsum00  12086  fsumabs  12089  fsumrelem  12095  fsumiun  12101  isumshft  12114  mertenslem2  12160  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  prodfct  12211  prodssdc  12213  fprodmul  12215  fprodm1s  12225  fprodp1s  12226  fprodcl2lem  12229  fprodabs  12240  fprod2dlemstep  12246  fprodcom2fi  12250  fprodrec  12253  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  fprodle  12264  pcmpt  12979  pcmptdvds  12981  gsumfzfsumlemm  14666  iuncld  14909  fsumcncntop  15361  dvmptfsum  15519