![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfrel2 | Structured version Visualization version GIF version |
Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
dfrel2 | ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv 5934 | . . 3 ⊢ Rel ◡◡𝑅 | |
2 | vex 3444 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | vex 3444 | . . . . . 6 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opelcnv 5716 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝑅) |
5 | 3, 2 | opelcnv 5716 | . . . . 5 ⊢ (〈𝑦, 𝑥〉 ∈ ◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
6 | 4, 5 | bitri 278 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
7 | 6 | eqrelriv 5626 | . . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅) |
8 | 1, 7 | mpan 689 | . 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅) |
9 | releq 5615 | . . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅)) | |
10 | 1, 9 | mpbii 236 | . 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅) |
11 | 8, 10 | impbii 212 | 1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1538 ∈ wcel 2111 〈cop 4531 ◡ccnv 5518 Rel wrel 5524 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-rel 5526 df-cnv 5527 |
This theorem is referenced by: dfrel4v 6014 cnvcnv 6016 cnveqb 6020 dfrel3 6022 cnvcnvres 6029 cnvsng 6047 cores2 6079 co01 6081 coi2 6083 relcnvtrg 6086 funcnvres2 6404 f1cnvcnv 6559 f1ocnv 6602 f1ocnvb 6603 f1ococnv1 6618 fimacnvinrn 6817 isores1 7066 relcnvexb 7613 cnvf1o 7789 fnwelem 7808 tposf12 7900 ssenen 8675 cantnffval2 9142 fsumcnv 15120 fprodcnv 15329 structcnvcnv 16489 imasless 16805 oppcinv 17042 cnvps 17814 cnvpsb 17815 cnvtsr 17824 gimcnv 18399 lmimcnv 19832 hmeocnv 22367 hmeocnvb 22379 cmphaushmeo 22405 ustexsym 22821 pi1xfrcnv 23662 dvlog 25242 efopnlem2 25248 gtiso 30460 cycpmconjvlem 30833 cycpmconjs 30848 f1ocan2fv 35165 relcnveq3 35738 relcnveq2 35740 brcnvrabga 35759 dfrel5 35763 elrelscnveq3 35891 elrelscnveq2 35893 ltrncnvnid 37423 relintab 40283 cnvssb 40286 relnonrel 40287 cononrel1 40294 cononrel2 40295 clrellem 40322 clcnvlem 40323 relexpaddss 40419 |
Copyright terms: Public domain | W3C validator |