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  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  nfop  3872  pofun  4402  nfse  4431  rabxfrd  4559  mptfvex  5719  fvmptf  5726  fmptcof  5801  fliftfuns  5921  riota2f  5976  ovmpos  6127  ov2gf  6128  elovmporab  6204  elovmporab1w  6205  fmpox  6344  mpofvex  6349  qliftfuns  6764  xpf1o  7001  iunfidisj  7109  cc3  7450  infssuzcldc  10450  sumfct  11880  sumrbdclem  11883  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsumsplitf  11914  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fisum0diag2  11953  fsummulc2  11954  fsum00  11968  fsumabs  11971  fsumrelem  11977  fsumiun  11983  isumshft  11996  mertenslem2  12042  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  prodfct  12093  prodssdc  12095  fprodmul  12097  fprodm1s  12107  fprodp1s  12108  fprodcl2lem  12111  fprodabs  12122  fprod2dlemstep  12128  fprodcom2fi  12132  fprodrec  12135  fproddivapf  12137  fprodsplitf  12138  fprodsplit1f  12140  fprodle  12146  pcmpt  12861  pcmptdvds  12863  gsumfzfsumlemm  14545  iuncld  14783  fsumcncntop  15235  dvmptfsum  15393