![]() |
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 5694 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 4230 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 4014 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3462 ∩ cin 3946 ⊆ wss 3947 × cxp 5680 ↾ cres 5684 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-in 3954 df-ss 3964 df-res 5694 |
This theorem is referenced by: dmresss 6020 rnresss 6026 relssres 6031 resexg 6036 iss 6044 mptss 6051 relresfld 6287 funres 6601 funres11 6636 funcnvres 6637 2elresin 6682 fssres 6768 foimacnv 6860 frxp 8140 fnwelem 8145 tposss 8242 dftpos4 8260 smores 8382 smores2 8384 tfrlem15 8422 finresfin 9304 imafi 9355 fidomdm 9376 marypha1lem 9476 hartogslem1 9585 r0weon 10055 ackbij2lem3 10284 axdc3lem2 10494 dmct 10567 smobeth 10629 wunres 10774 vdwnnlem1 16997 symgsssg 19465 symgfisg 19466 psgnunilem5 19492 odf1o2 19571 gsumzres 19907 gsumzaddlem 19919 gsumzadd 19920 gsum2dlem2 19969 dprdfadd 20020 dprdres 20028 dprd2dlem1 20041 dprd2da 20042 lindfres 21821 opsrtoslem2 22069 txss12 23600 txbasval 23601 fmss 23941 ustneism 24219 trust 24225 isngp2 24597 equivcau 25319 metsscmetcld 25334 volf 25549 dvcnvrelem1 26041 tdeglem4OLD 26087 pserdv 26459 dvlog 26678 dchrelbas2 27266 issubgr2 29208 subgrprop2 29210 uhgrspansubgr 29227 hlimadd 31126 hlimcaui 31169 hhssabloilem 31194 hhsst 31199 hhsssh2 31203 hhsscms 31211 occllem 31236 nlelchi 31994 hmopidmchi 32084 fnresin 32543 fressupp 32600 imafi2 32625 pfxrn2 32803 omsmon 34132 carsggect 34152 eulerpartlemmf 34209 funpartss 35768 brresi2 37421 bnd2lem 37492 idresssidinxp 38006 disjimres 38448 aks6d1c2 41828 eqresfnbd 41956 diophrw 42416 dnnumch2 42706 lmhmlnmsplit 42748 hbtlem6 42790 dfrcl2 43341 relexpaddss 43385 cotrclrcl 43409 frege131d 43431 resimass 44848 fourierdlem42 45770 fourierdlem80 45807 isubgrsubgr 47434 setrecsres 48448 |
Copyright terms: Public domain | W3C validator |