| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sselii | Structured version Visualization version GIF version | ||
| Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
| Ref | Expression |
|---|---|
| sseli.1 | ⊢ 𝐴 ⊆ 𝐵 |
| sselii.2 | ⊢ 𝐶 ∈ 𝐴 |
| Ref | Expression |
|---|---|
| sselii | ⊢ 𝐶 ∈ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sselii.2 | . 2 ⊢ 𝐶 ∈ 𝐴 | |
| 2 | sseli.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
| 3 | 2 | sseli 3979 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐶 ∈ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ⊆ wss 3951 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 df-ss 3968 |
| This theorem is referenced by: sseliALT 5309 fvrn0 6936 ovima0 7612 brtpos0 8258 frrlem14 8324 wfrlem16OLD 8364 rdg0 8461 iunfi 9383 rankdmr1 9841 rankeq0b 9900 cardprclem 10019 alephfp2 10149 dfac2b 10171 sdom2en01 10342 fin56 10433 fin1a2lem10 10449 hsmexlem4 10469 canthp1lem2 10693 ax1cn 11189 recni 11275 0xr 11308 pnfxr 11315 nn0rei 12537 nn0cni 12538 0xnn0 12605 nnzi 12641 nn0zi 12642 seqexw 14058 mulgfval 19087 lbsextlem4 21163 qsubdrg 21437 leordtval2 23220 iooordt 23225 hauspwdom 23509 comppfsc 23540 dfac14 23626 filconn 23891 isufil2 23916 iooretop 24786 ovolfiniun 25536 volfiniun 25582 iblabslem 25863 iblabs 25864 bddmulibl 25874 mdegcl 26108 logcn 26689 logccv 26705 leibpi 26985 xrlimcnp 27011 jensen 27032 emre 27049 lgsdir2lem3 27371 shelii 31234 chelii 31252 omlsilem 31421 nonbooli 31670 pjssmii 31700 riesz4 32083 riesz1 32084 cnlnadjeu 32097 nmopadjlei 32107 adjeq0 32110 dp2clq 32863 rpdp2cl 32864 dp2lt10 32866 dp2lt 32867 dp2ltc 32869 dplti 32887 zringfrac 33582 qqh0 33985 qqh1 33986 qqhcn 33992 rrh0 34016 esumcst 34064 esumrnmpt2 34069 volmeas 34232 hgt750lem 34666 tgoldbachgtde 34675 kur14lem7 35217 kur14lem9 35219 iinllyconn 35259 bj-rdg0gALT 37072 bj-pinftyccb 37222 bj-minftyccb 37226 bj-rrdrg 37291 finixpnum 37612 poimirlem32 37659 ftc1cnnclem 37698 ftc2nc 37709 areacirclem2 37716 prdsbnd 37800 reheibor 37846 rmxyadd 42933 rmxy1 42934 rmxy0 42935 rmydioph 43026 rmxdioph 43028 expdiophlem2 43034 expdioph 43035 mpaaeu 43162 0iscard 43554 1iscard 43555 wfaxrep 45011 wfaxnul 45013 wfaxinf2 45018 fourierdlem85 46206 fourierdlem102 46223 fourierdlem114 46235 iooborel 46366 hoicvrrex 46571 |
| Copyright terms: Public domain | W3C validator |