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 4129 | . 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∩ cin 3886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 |
This theorem is referenced by: ordtypelem3 9279 ordtypelem4 9280 ordtypelem7 9283 infpwfien 9818 ttukeylem6 10270 fpwwe2lem11 10397 explecnv 15577 smuval2 16189 submrc 17337 coffth 17652 catcbascl 17827 catcoppcclOLD 17833 catcfucclOLD 17835 catcxpcclOLD 17925 acsfiindd 18271 frgpnabllem2 19475 ablfac2 19692 zringlpirlem2 20685 mplind 21278 neiptoptop 22282 restbas 22309 subbascn 22405 cnconn 22573 clsconn 22581 conncompclo 22586 cldllycmp 22646 llycmpkgen2 22701 1stckgenlem 22704 txcls 22755 txcnp 22771 ptcnplem 22772 xkopt 22806 txconn 22840 basqtop 22862 tgqtop 22863 kqnrmlem1 22894 kqnrmlem2 22895 nrmhmph 22945 ptcmplem5 23207 restutop 23389 blin2 23582 met2ndci 23678 zdis 23979 reconnlem2 23990 cnheibor 24118 lebnum 24127 nmoleub2lem 24277 nmoleub2lem3 24278 nmoleub2lem2 24279 nmoleub3 24282 nmhmcn 24283 minveclem4 24596 ovolicc2lem5 24685 ioorcl 24741 ig1peu 25336 taylfvallem1 25516 tayl0 25521 ppisval 26253 ppinprm 26301 chtnprm 26303 chtleppi 26358 pclogsum 26363 chpchtsum 26367 chpub 26368 chebbnd1lem1 26617 chtppilimlem1 26621 rplogsum 26675 perpcom 27074 perpneq 27075 ragperp 27078 tocyc01 31385 cyc3evpm 31417 cycpmgcl 31420 cycpmconjslem2 31422 cyc3conja 31424 lbsdiflsp0 31707 esum2d 32061 ispisys2 32121 sigapisys 32123 sigapildsyslem 32129 sigapildsys 32130 eulerpartlemgvv 32343 tgoldbachgt 32643 fvineqsneq 35583 pibt2 35588 limclner 43192 thincciso 46330 |
Copyright terms: Public domain | W3C validator |