![]() |
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 3891 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐶 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2083 ⊆ wss 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-in 3872 df-ss 3880 |
This theorem is referenced by: sseliALT 5111 fvrn0 6573 ovima0 7190 brtpos0 7757 wfrlem16 7829 rdg0 7916 iunfi 8665 rankdmr1 9083 rankeq0b 9142 cardprclem 9261 alephfp2 9388 dfac2b 9409 sdom2en01 9577 fin56 9668 fin1a2lem10 9684 hsmexlem4 9704 canthp1lem2 9928 ax1cn 10424 recni 10508 0xr 10541 pnfxr 10548 nn0rei 11762 nn0cni 11763 0xnn0 11827 nnzi 11860 nn0zi 11861 seqexw 13239 mulgfval 17987 lbsextlem4 19627 qsubdrg 20283 leordtval2 21508 iooordt 21513 hauspwdom 21797 comppfsc 21828 dfac14 21914 filconn 22179 isufil2 22204 iooretop 23061 ovolfiniun 23789 volfiniun 23835 iblabslem 24115 iblabs 24116 bddmulibl 24126 mdegcl 24350 logcn 24915 logccv 24931 leibpi 25206 xrlimcnp 25232 jensen 25252 emre 25269 lgsdir2lem3 25589 shelii 28679 chelii 28697 omlsilem 28866 nonbooli 29115 pjssmii 29145 riesz4 29528 riesz1 29529 cnlnadjeu 29542 nmopadjlei 29552 adjeq0 29555 dp2clq 30237 rpdp2cl 30238 dp2lt10 30240 dp2lt 30241 dp2ltc 30243 dplti 30261 qqh0 30838 qqh1 30839 qqhcn 30845 rrh0 30869 esumcst 30935 esumrnmpt2 30940 volmeas 31103 hgt750lem 31535 tgoldbachgtde 31544 kur14lem7 32069 kur14lem9 32071 iinllyconn 32111 frrlem14 32747 bj-pinftyccb 34082 bj-minftyccb 34086 finixpnum 34429 poimirlem32 34476 ftc1cnnclem 34517 ftc2nc 34528 areacirclem2 34535 prdsbnd 34624 reheibor 34670 rmxyadd 39024 rmxy1 39025 rmxy0 39026 rmydioph 39117 rmxdioph 39119 expdiophlem2 39125 expdioph 39126 mpaaeu 39256 fourierdlem85 42040 fourierdlem102 42057 fourierdlem114 42069 iooborel 42198 hoicvrrex 42402 |
Copyright terms: Public domain | W3C validator |