| 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 4201 | . 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 |
| This theorem is referenced by: ordtypelem3 9560 ordtypelem4 9561 ordtypelem7 9564 infpwfien 10102 ttukeylem6 10554 fpwwe2lem11 10681 explecnv 15901 smuval2 16519 submrc 17671 coffth 17983 catcbascl 18157 acsfiindd 18598 frgpnabllem2 19892 ablfac2 20109 idomcringd 20727 2idllidld 21264 zringlpirlem2 21474 mplind 22094 neiptoptop 23139 restbas 23166 subbascn 23262 cnconn 23430 clsconn 23438 conncompclo 23443 cldllycmp 23503 llycmpkgen2 23558 1stckgenlem 23561 txcls 23612 txcnp 23628 ptcnplem 23629 xkopt 23663 txconn 23697 basqtop 23719 tgqtop 23720 kqnrmlem1 23751 kqnrmlem2 23752 nrmhmph 23802 ptcmplem5 24064 restutop 24246 blin2 24439 met2ndci 24535 zdis 24838 reconnlem2 24849 cnheibor 24987 lebnum 24996 nmoleub2lem 25147 nmoleub2lem3 25148 nmoleub2lem2 25149 nmoleub3 25152 nmhmcn 25153 minveclem4 25466 ovolicc2lem5 25556 ioorcl 25612 ig1peu 26214 taylfvallem1 26398 tayl0 26403 ppisval 27147 ppinprm 27195 chtnprm 27197 chtleppi 27254 pclogsum 27259 chpchtsum 27263 chpub 27264 chebbnd1lem1 27513 chtppilimlem1 27517 rplogsum 27571 perpcom 28721 perpneq 28722 ragperp 28725 tocyc01 33138 cyc3evpm 33170 cycpmgcl 33173 cycpmconjslem2 33175 cyc3conja 33177 idomrcanOLD 33285 unitpidl1 33452 ssdifidlprm 33486 mxidlirredi 33499 mxidlirred 33500 rprmirredb 33560 pidufd 33571 1arithufdlem4 33575 exsslsb 33647 lbsdiflsp0 33677 esum2d 34094 ispisys2 34154 sigapisys 34156 sigapildsyslem 34162 sigapildsys 34163 eulerpartlemgvv 34378 tgoldbachgt 34678 weiunfrlem 36465 weiunfr 36468 fvineqsneq 37413 pibt2 37418 limclner 45666 thincciso 49102 termcterm2 49146 |
| Copyright terms: Public domain | W3C validator |