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 5561 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 4204 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 4000 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3495 ∩ cin 3934 ⊆ wss 3935 × cxp 5547 ↾ cres 5551 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-in 3942 df-ss 3951 df-res 5561 |
This theorem is referenced by: relssres 5887 resexg 5892 iss 5897 mptss 5904 relresfld 6121 funres 6391 funres11 6425 funcnvres 6426 2elresin 6462 fssres 6538 foimacnv 6626 frxp 7811 fnwelem 7816 tposss 7884 dftpos4 7902 smores 7980 smores2 7982 tfrlem15 8019 finresfin 8733 fidomdm 8790 imafi 8806 marypha1lem 8886 hartogslem1 8995 r0weon 9427 ackbij2lem3 9652 axdc3lem2 9862 dmct 9935 smobeth 9997 wunres 10142 vdwnnlem1 16321 symgsssg 18526 symgfisg 18527 psgnunilem5 18553 odf1o2 18629 gsumzres 18960 gsumzaddlem 18972 gsumzadd 18973 gsum2dlem2 19022 dprdfadd 19073 dprdres 19081 dprd2dlem1 19094 dprd2da 19095 opsrtoslem2 20195 lindfres 20897 txss12 22143 txbasval 22144 fmss 22484 ustneism 22761 trust 22767 isngp2 23135 equivcau 23832 metsscmetcld 23847 volf 24059 dvcnvrelem1 24543 tdeglem4 24583 pserdv 24946 dvlog 25161 dchrelbas2 25741 issubgr2 26982 subgrprop2 26984 uhgrspansubgr 27001 hlimadd 28898 hlimcaui 28941 hhssabloilem 28966 hhsst 28971 hhsssh2 28975 hhsscms 28983 occllem 29008 nlelchi 29766 hmopidmchi 29856 fnresin 30300 imafi2 30374 pfxrn2 30544 omsmon 31456 carsggect 31476 eulerpartlemmf 31533 funpartss 33303 brresi2 34877 bnd2lem 34952 idresssidinxp 35449 disjimres 35862 diophrw 39236 dnnumch2 39525 lmhmlnmsplit 39567 hbtlem6 39609 dfrcl2 39899 relexpaddss 39943 cotrclrcl 39967 frege131d 39989 rnresss 41319 resimass 41390 fourierdlem42 42315 fourierdlem80 42352 setrecsres 44702 |
Copyright terms: Public domain | W3C validator |