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 5050 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 3795 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3598 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3173 ∩ cin 3539 ⊆ wss 3540 × cxp 5036 ↾ cres 5040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-res 5050 |
This theorem is referenced by: relssres 5357 resexg 5362 iss 5367 mptss 5373 relresfld 5579 funres 5843 funres11 5880 funcnvres 5881 2elresin 5916 fssres 5983 foimacnv 6067 frxp 7174 fnwelem 7179 tposss 7240 dftpos4 7258 smores 7336 smores2 7338 tfrlem15 7375 finresfin 8071 fidomdm 8128 imafi 8142 marypha1lem 8222 hartogslem1 8330 r0weon 8718 ackbij2lem3 8946 axdc3lem2 9156 smobeth 9287 wunres 9432 vdwnnlem1 15537 symgsssg 17710 symgfisg 17711 psgnunilem5 17737 odf1o2 17811 gsumzres 18133 gsumzaddlem 18144 gsumzadd 18145 gsum2dlem2 18193 dprdfadd 18242 dprdres 18250 dprd2dlem1 18263 dprd2da 18264 opsrtoslem2 19306 lindfres 19981 txss12 21218 txbasval 21219 fmss 21560 ustneism 21837 trust 21843 isngp2 22211 equivcau 22906 cmetss 22921 volf 23104 dvcnvrelem1 23584 tdeglem4 23624 pserdv 23987 dvlog 24197 dchrelbas2 24762 uhgrares 25837 umgrares 25853 usgrares 25898 hlimadd 27434 hlimcaui 27477 hhssabloilem 27502 hhsst 27507 hhsssh2 27511 hhsscms 27520 occllem 27546 nlelchi 28304 hmopidmchi 28394 fnresin 28812 imafi2 28872 dmct 28877 omsmon 29687 carsggect 29707 eulerpartlemmf 29764 nodenselem6 31085 funpartss 31221 brresi 32683 bnd2lem 32760 diophrw 36340 dnnumch2 36633 lmhmlnmsplit 36675 hbtlem6 36718 dfrcl2 36985 relexpaddss 37029 cotrclrcl 37053 frege131d 37075 rnresss 38360 fourierdlem42 39042 fourierdlem80 39079 resisresindm 40320 issubgr2 40496 subgrprop2 40498 uhgrspansubgr 40515 |
Copyright terms: Public domain | W3C validator |