![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfrel2 | Structured version Visualization version Unicode version |
Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
dfrel2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv 5229 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | vex 3060 |
. . . . . 6
![]() ![]() ![]() ![]() | |
3 | vex 3060 |
. . . . . 6
![]() ![]() ![]() ![]() | |
4 | 2, 3 | opelcnv 5038 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 2 | opelcnv 5038 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 4, 5 | bitri 257 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | eqrelriv 4950 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | mpan 681 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | releq 4939 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 1, 9 | mpbii 216 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 8, 10 | impbii 192 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4541 ax-nul 4550 ax-pr 4656 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4419 df-opab 4478 df-xp 4862 df-rel 4863 df-cnv 4864 |
This theorem is referenced by: dfrel4v 5309 cnvcnv 5311 cnveqb 5314 dfrel3 5316 cnvcnvres 5322 cnvsn 5342 cores2 5371 co01 5373 coi2 5375 relcnvtr 5378 funcnvres2 5680 f1cnvcnv 5814 f1ocnv 5853 f1ocnvb 5854 f1ococnv1 5869 isores1 6255 relcnvexb 6773 cnvf1o 6927 fnwelem 6943 tposf12 7029 ssenen 7777 cantnffval2 8231 fsumcnv 13889 fprodcnv 14092 structcnvcnv 15187 imasless 15501 oppcinv 15740 cnvps 16513 cnvpsb 16514 cnvtsr 16523 gimcnv 16986 lmimcnv 18345 hmeocnv 20832 hmeocnvb 20844 cmphaushmeo 20870 ustexsym 21285 pi1xfrcnv 22143 dvlog 23652 efopnlem2 23658 fimacnvinrn 28288 gtiso 28333 f1ocan2fv 32100 ltrncnvnid 33738 relintab 36235 cnvssb 36238 relnonrel 36239 cononrel1 36246 cononrel2 36247 clrellem 36275 clcnvlem 36276 relexpaddss 36356 |
Copyright terms: Public domain | W3C validator |