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 3962 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐶 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ⊆ wss 3935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3942 df-ss 3951 |
This theorem is referenced by: sseliALT 5205 fvrn0 6692 ovima0 7321 brtpos0 7893 wfrlem16 7964 rdg0 8051 iunfi 8806 rankdmr1 9224 rankeq0b 9283 cardprclem 9402 alephfp2 9529 dfac2b 9550 sdom2en01 9718 fin56 9809 fin1a2lem10 9825 hsmexlem4 9845 canthp1lem2 10069 ax1cn 10565 recni 10649 0xr 10682 pnfxr 10689 nn0rei 11902 nn0cni 11903 0xnn0 11967 nnzi 12000 nn0zi 12001 seqexw 13379 mulgfval 18220 lbsextlem4 19927 qsubdrg 20591 leordtval2 21814 iooordt 21819 hauspwdom 22103 comppfsc 22134 dfac14 22220 filconn 22485 isufil2 22510 iooretop 23368 ovolfiniun 24096 volfiniun 24142 iblabslem 24422 iblabs 24423 bddmulibl 24433 mdegcl 24657 logcn 25224 logccv 25240 leibpi 25514 xrlimcnp 25540 jensen 25560 emre 25577 lgsdir2lem3 25897 shelii 28986 chelii 29004 omlsilem 29173 nonbooli 29422 pjssmii 29452 riesz4 29835 riesz1 29836 cnlnadjeu 29849 nmopadjlei 29859 adjeq0 29862 dp2clq 30552 rpdp2cl 30553 dp2lt10 30555 dp2lt 30556 dp2ltc 30558 dplti 30576 qqh0 31220 qqh1 31221 qqhcn 31227 rrh0 31251 esumcst 31317 esumrnmpt2 31322 volmeas 31485 hgt750lem 31917 tgoldbachgtde 31926 kur14lem7 32454 kur14lem9 32456 iinllyconn 32496 frrlem14 33131 bj-pinftyccb 34497 bj-minftyccb 34501 bj-rrdrg 34565 finixpnum 34871 poimirlem32 34918 ftc1cnnclem 34959 ftc2nc 34970 areacirclem2 34977 prdsbnd 35065 reheibor 35111 rmxyadd 39511 rmxy1 39512 rmxy0 39513 rmydioph 39604 rmxdioph 39606 expdiophlem2 39612 expdioph 39613 mpaaeu 39743 fourierdlem85 42470 fourierdlem102 42487 fourierdlem114 42499 iooborel 42628 hoicvrrex 42832 |
Copyright terms: Public domain | W3C validator |