![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relres | Structured version Visualization version Unicode version |
Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
relres |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 4864 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | inss2 3664 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqsstri 3473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | relxp 4960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | relss 4940 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | mp2 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 df-ss 3429 df-opab 4475 df-xp 4858 df-rel 4859 df-res 4864 |
This theorem is referenced by: elres 5158 iss 5170 dfres2 5175 restidsing 5179 issref 5231 asymref 5234 poirr2 5242 cnvcnvres 5317 resco 5357 coeq0 5362 ressn 5390 funssres 5640 fnresdisj 5707 fnres 5713 fresaunres2 5777 fcnvres 5782 nfunsn 5918 dffv2 5960 fsnunfv 6127 resiexg 6755 resfunexgALT 6782 domss2 7756 fidomdm 7878 relexp0rel 13148 setsres 15199 pospo 16267 metustid 21617 ovoliunlem1 22503 dvres 22914 dvres2 22915 dvlog 23644 efopnlem2 23650 h2hlm 26681 hlimcaui 26937 dmct 28346 dfpo2 30443 dfrdg2 30490 funpartfun 30758 mapfzcons1 35603 diophrw 35645 eldioph2lem1 35646 eldioph2lem2 35647 undmrnresiss 36254 rtrclexi 36272 brfvrcld2 36328 relexpiidm 36340 rp-imass 36410 idhe 36427 funressnfv 38666 dfdfat2 38670 |
Copyright terms: Public domain | W3C validator |