Theorem nfel1 2383

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

Syntax hints:  Ⅎwnf 1506   ∈ wcel 2200  Ⅎwnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  vtocl2gf  2864  vtocl3gf  2865  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  nfop  3876  pofun  4407  nfse  4436  rabxfrd  4564  mptfvex  5728  fvmptf  5735  fmptcof  5810  fliftfuns  5934  riota2f  5989  ovmpos  6140  ov2gf  6141  elovmporab  6217  elovmporab1w  6218  fmpox  6360  mpofvex  6365  qliftfuns  6783  xpf1o  7025  iunfidisj  7136  cc3  7477  infssuzcldc  10485  sumfct  11925  sumrbdclem  11928  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsumsplitf  11959  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fisum0diag2  11998  fsummulc2  11999  fsum00  12013  fsumabs  12016  fsumrelem  12022  fsumiun  12028  isumshft  12041  mertenslem2  12087  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  prodfct  12138  prodssdc  12140  fprodmul  12142  fprodm1s  12152  fprodp1s  12153  fprodcl2lem  12156  fprodabs  12167  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  fprodle  12191  pcmpt  12906  pcmptdvds  12908  gsumfzfsumlemm  14591  iuncld  14829  fsumcncntop  15281  dvmptfsum  15439