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 4085 | . 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ∩ cin 3842 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-in 3850 |
This theorem is referenced by: ordtypelem3 9059 ordtypelem4 9060 ordtypelem7 9063 infpwfien 9564 ttukeylem6 10016 fpwwe2lem11 10143 explecnv 15315 smuval2 15927 submrc 17004 coffth 17313 catcoppccl 17486 catcfuccl 17487 catcxpccl 17575 acsfiindd 17905 frgpnabllem2 19115 ablfac2 19332 zringlpirlem2 20306 mplind 20884 neiptoptop 21884 restbas 21911 subbascn 22007 cnconn 22175 clsconn 22183 conncompclo 22188 cldllycmp 22248 llycmpkgen2 22303 1stckgenlem 22306 txcls 22357 txcnp 22373 ptcnplem 22374 xkopt 22408 txconn 22442 basqtop 22464 tgqtop 22465 kqnrmlem1 22496 kqnrmlem2 22497 nrmhmph 22547 ptcmplem5 22809 restutop 22991 blin2 23184 met2ndci 23277 zdis 23570 reconnlem2 23581 cnheibor 23709 lebnum 23718 nmoleub2lem 23868 nmoleub2lem3 23869 nmoleub2lem2 23870 nmoleub3 23873 nmhmcn 23874 minveclem4 24186 ovolicc2lem5 24275 ioorcl 24331 ig1peu 24926 taylfvallem1 25106 tayl0 25111 ppisval 25843 ppinprm 25891 chtnprm 25893 chtleppi 25948 pclogsum 25953 chpchtsum 25957 chpub 25958 chebbnd1lem1 26207 chtppilimlem1 26211 rplogsum 26265 perpcom 26661 perpneq 26662 ragperp 26665 tocyc01 30964 cyc3evpm 30996 cycpmgcl 30999 cycpmconjslem2 31001 cyc3conja 31003 lbsdiflsp0 31281 esum2d 31633 ispisys2 31693 sigapisys 31695 sigapildsyslem 31701 sigapildsys 31702 eulerpartlemgvv 31915 tgoldbachgt 32215 fvineqsneq 35228 pibt2 35233 limclner 42756 |
Copyright terms: Public domain | W3C validator |