Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elin1d | Structured version Visualization version GIF version |
Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
Ref | Expression |
---|---|
elin1d.1 | ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) |
Ref | Expression |
---|---|
elin1d | ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin1d.1 | . 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) | |
2 | elinel1 4169 | . 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ∩ cin 3932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 |
This theorem is referenced by: ordtypelem3 8972 ordtypelem4 8973 ordtypelem7 8976 infpwfien 9476 ttukeylem6 9924 fpwwe2lem12 10051 explecnv 15208 smuval2 15819 submrc 16887 coffth 17194 catcoppccl 17356 catcfuccl 17357 catcxpccl 17445 acsfiindd 17775 frgpnabllem2 18923 ablfac2 19140 mplind 20210 zringlpirlem2 20560 neiptoptop 21667 restbas 21694 subbascn 21790 cnconn 21958 clsconn 21966 conncompclo 21971 cldllycmp 22031 llycmpkgen2 22086 1stckgenlem 22089 txcls 22140 txcnp 22156 ptcnplem 22157 xkopt 22191 txconn 22225 basqtop 22247 tgqtop 22248 kqnrmlem1 22279 kqnrmlem2 22280 nrmhmph 22330 ptcmplem5 22592 restutop 22773 blin2 22966 met2ndci 23059 zdis 23351 reconnlem2 23362 cnheibor 23486 lebnum 23495 nmoleub2lem 23645 nmoleub2lem3 23646 nmoleub2lem2 23647 nmoleub3 23650 nmhmcn 23651 minveclem4 23962 ovolicc2lem5 24049 ioorcl 24105 ig1peu 24692 taylfvallem1 24872 tayl0 24877 ppisval 25608 ppinprm 25656 chtnprm 25658 chtleppi 25713 pclogsum 25718 chpchtsum 25722 chpub 25723 chebbnd1lem1 25972 chtppilimlem1 25976 rplogsum 26030 perpcom 26426 perpneq 26427 ragperp 26430 tocyc01 30687 cyc3evpm 30719 cycpmgcl 30722 cycpmconjslem2 30724 cyc3conja 30726 lbsdiflsp0 30921 esum2d 31251 ispisys2 31311 sigapisys 31313 sigapildsyslem 31319 sigapildsys 31320 eulerpartlemgvv 31533 tgoldbachgt 31833 fvineqsneq 34575 pibt2 34580 limclner 41808 |
Copyright terms: Public domain | W3C validator |