Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resss | Structured version Visualization version GIF version |
Description: A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
resss | ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 5560 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 4202 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3998 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3492 ∩ cin 3932 ⊆ wss 3933 × cxp 5546 ↾ cres 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-ss 3949 df-res 5560 |
This theorem is referenced by: relssres 5886 resexg 5891 iss 5896 mptss 5903 relresfld 6120 funres 6390 funres11 6424 funcnvres 6425 2elresin 6461 fssres 6537 foimacnv 6625 frxp 7809 fnwelem 7814 tposss 7882 dftpos4 7900 smores 7978 smores2 7980 tfrlem15 8017 finresfin 8732 fidomdm 8789 imafi 8805 marypha1lem 8885 hartogslem1 8994 r0weon 9426 ackbij2lem3 9651 axdc3lem2 9861 dmct 9934 smobeth 9996 wunres 10141 vdwnnlem1 16319 symgsssg 18524 symgfisg 18525 psgnunilem5 18551 odf1o2 18627 gsumzres 18958 gsumzaddlem 18970 gsumzadd 18971 gsum2dlem2 19020 dprdfadd 19071 dprdres 19079 dprd2dlem1 19092 dprd2da 19093 opsrtoslem2 20193 lindfres 20895 txss12 22141 txbasval 22142 fmss 22482 ustneism 22759 trust 22765 isngp2 23133 equivcau 23830 metsscmetcld 23845 volf 24057 dvcnvrelem1 24541 tdeglem4 24581 pserdv 24944 dvlog 25161 dchrelbas2 25740 issubgr2 26981 subgrprop2 26983 uhgrspansubgr 27000 hlimadd 28897 hlimcaui 28940 hhssabloilem 28965 hhsst 28970 hhsssh2 28974 hhsscms 28982 occllem 29007 nlelchi 29765 hmopidmchi 29855 fnresin 30299 imafi2 30373 pfxrn2 30543 omsmon 31455 carsggect 31475 eulerpartlemmf 31532 funpartss 33302 brresi2 34875 bnd2lem 34950 idresssidinxp 35447 disjimres 35860 diophrw 39234 dnnumch2 39523 lmhmlnmsplit 39565 hbtlem6 39607 dfrcl2 39897 relexpaddss 39941 cotrclrcl 39965 frege131d 39987 rnresss 41315 resimass 41386 fourierdlem42 42311 fourierdlem80 42348 setrecsres 44732 |
Copyright terms: Public domain | W3C validator |