|   | 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 5696 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
| 2 | inss1 4236 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
| 3 | 1, 2 | eqsstri 4029 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: Vcvv 3479 ∩ cin 3949 ⊆ wss 3950 × cxp 5682 ↾ cres 5686 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-in 3957 df-ss 3967 df-res 5696 | 
| This theorem is referenced by: dmresss 6028 rnresss 6034 relssres 6039 resexg 6044 iss 6052 mptss 6059 relresfld 6295 funres 6607 funres11 6642 funcnvres 6643 2elresin 6688 fssres 6773 foimacnv 6864 frxp 8152 fnwelem 8157 tposss 8253 dftpos4 8271 smores 8393 smores2 8395 tfrlem15 8433 finresfin 9305 imafi 9354 fidomdm 9375 marypha1lem 9474 hartogslem1 9583 r0weon 10053 ackbij2lem3 10281 axdc3lem2 10492 dmct 10565 smobeth 10627 wunres 10772 vdwnnlem1 17034 symgsssg 19486 symgfisg 19487 psgnunilem5 19513 odf1o2 19592 gsumzres 19928 gsumzaddlem 19940 gsumzadd 19941 gsum2dlem2 19990 dprdfadd 20041 dprdres 20049 dprd2dlem1 20062 dprd2da 20063 lindfres 21844 opsrtoslem2 22081 txss12 23614 txbasval 23615 fmss 23955 ustneism 24233 trust 24239 isngp2 24611 equivcau 25335 metsscmetcld 25350 volf 25565 dvcnvrelem1 26057 pserdv 26474 dvlog 26694 dchrelbas2 27282 issubgr2 29290 subgrprop2 29292 uhgrspansubgr 29309 hlimadd 31213 hlimcaui 31256 hhssabloilem 31281 hhsst 31286 hhsssh2 31290 hhsscms 31298 occllem 31323 nlelchi 32081 hmopidmchi 32171 fnresin 32637 fressupp 32698 imafi2 32724 pfxrn2 32925 omsmon 34301 carsggect 34321 eulerpartlemmf 34378 funpartss 35946 brresi2 37728 bnd2lem 37799 idresssidinxp 38310 disjimres 38752 aks6d1c2 42132 eqresfnbd 42273 diophrw 42775 dnnumch2 43062 lmhmlnmsplit 43104 hbtlem6 43146 dfrcl2 43692 relexpaddss 43736 cotrclrcl 43760 frege131d 43782 resimass 45251 fourierdlem42 46169 fourierdlem80 46206 isubgredgss 47856 isubgrsubgr 47860 setrecsres 49276 | 
| Copyright terms: Public domain | W3C validator |