![]() |
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 3972 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐶 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802 df-ss 3961 |
This theorem is referenced by: sseliALT 5310 fvrn0 6926 ovima0 7600 brtpos0 8239 frrlem14 8305 wfrlem16OLD 8345 rdg0 8442 iunfi 9366 rankdmr1 9826 rankeq0b 9885 cardprclem 10004 alephfp2 10134 dfac2b 10155 sdom2en01 10327 fin56 10418 fin1a2lem10 10434 hsmexlem4 10454 canthp1lem2 10678 ax1cn 11174 recni 11260 0xr 11293 pnfxr 11300 nn0rei 12516 nn0cni 12517 0xnn0 12583 nnzi 12619 nn0zi 12620 seqexw 14018 mulgfval 19033 lbsextlem4 21061 qsubdrg 21369 leordtval2 23160 iooordt 23165 hauspwdom 23449 comppfsc 23480 dfac14 23566 filconn 23831 isufil2 23856 iooretop 24726 ovolfiniun 25474 volfiniun 25520 iblabslem 25801 iblabs 25802 bddmulibl 25812 mdegcl 26049 logcn 26626 logccv 26642 leibpi 26919 xrlimcnp 26945 jensen 26966 emre 26983 lgsdir2lem3 27305 shelii 31097 chelii 31115 omlsilem 31284 nonbooli 31533 pjssmii 31563 riesz4 31946 riesz1 31947 cnlnadjeu 31960 nmopadjlei 31970 adjeq0 31973 dp2clq 32689 rpdp2cl 32690 dp2lt10 32692 dp2lt 32693 dp2ltc 32695 dplti 32713 zringfrac 33369 qqh0 33716 qqh1 33717 qqhcn 33723 rrh0 33747 esumcst 33813 esumrnmpt2 33818 volmeas 33981 hgt750lem 34414 tgoldbachgtde 34423 kur14lem7 34953 kur14lem9 34955 iinllyconn 34995 bj-rdg0gALT 36681 bj-pinftyccb 36831 bj-minftyccb 36835 bj-rrdrg 36900 finixpnum 37209 poimirlem32 37256 ftc1cnnclem 37295 ftc2nc 37306 areacirclem2 37313 prdsbnd 37397 reheibor 37443 rmxyadd 42484 rmxy1 42485 rmxy0 42486 rmydioph 42577 rmxdioph 42579 expdiophlem2 42585 expdioph 42586 mpaaeu 42716 0iscard 43113 1iscard 43114 fourierdlem85 45717 fourierdlem102 45734 fourierdlem114 45746 iooborel 45877 hoicvrrex 46082 |
Copyright terms: Public domain | W3C validator |