![]() |
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 5643 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss1 4186 | . 2 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3976 | 1 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3443 ∩ cin 3907 ⊆ wss 3908 × cxp 5629 ↾ cres 5633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-in 3915 df-ss 3925 df-res 5643 |
This theorem is referenced by: rnresss 5971 relssres 5976 resexg 5981 iss 5987 mptss 5994 relresfld 6226 funres 6540 funres11 6575 funcnvres 6576 2elresin 6619 fssres 6705 foimacnv 6798 frxp 8050 fnwelem 8055 tposss 8150 dftpos4 8168 smores 8290 smores2 8292 tfrlem15 8330 finresfin 9172 fidomdm 9231 imafiALT 9247 marypha1lem 9327 hartogslem1 9436 r0weon 9906 ackbij2lem3 10135 axdc3lem2 10345 dmct 10418 smobeth 10480 wunres 10625 vdwnnlem1 16827 symgsssg 19208 symgfisg 19209 psgnunilem5 19235 odf1o2 19314 gsumzres 19645 gsumzaddlem 19657 gsumzadd 19658 gsum2dlem2 19707 dprdfadd 19758 dprdres 19766 dprd2dlem1 19779 dprd2da 19780 lindfres 21182 opsrtoslem2 21415 txss12 22908 txbasval 22909 fmss 23249 ustneism 23527 trust 23533 isngp2 23905 equivcau 24616 metsscmetcld 24631 volf 24845 dvcnvrelem1 25333 tdeglem4OLD 25377 pserdv 25740 dvlog 25958 dchrelbas2 26537 issubgr2 28049 subgrprop2 28051 uhgrspansubgr 28068 hlimadd 29964 hlimcaui 30007 hhssabloilem 30032 hhsst 30037 hhsssh2 30041 hhsscms 30049 occllem 30074 nlelchi 30832 hmopidmchi 30922 fnresin 31369 fressupp 31430 imafi2 31454 pfxrn2 31622 omsmon 32710 carsggect 32730 eulerpartlemmf 32787 funpartss 34467 brresi2 36116 bnd2lem 36188 idresssidinxp 36707 disjimres 37150 diophrw 40991 dnnumch2 41281 lmhmlnmsplit 41323 hbtlem6 41365 dfrcl2 41857 relexpaddss 41901 cotrclrcl 41925 frege131d 41947 resimass 43371 fourierdlem42 44291 fourierdlem80 44328 setrecsres 47048 |
Copyright terms: Public domain | W3C validator |