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 5960 | . . 3 ⊢ Rel ◡◡𝑅 | |
2 | vex 3495 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | vex 3495 | . . . . . 6 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opelcnv 5745 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝑅) |
5 | 3, 2 | opelcnv 5745 | . . . . 5 ⊢ (〈𝑦, 𝑥〉 ∈ ◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
6 | 4, 5 | bitri 276 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
7 | 6 | eqrelriv 5655 | . . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅) |
8 | 1, 7 | mpan 686 | . 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅) |
9 | releq 5644 | . . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅)) | |
10 | 1, 9 | mpbii 234 | . 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅) |
11 | 8, 10 | impbii 210 | 1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ∈ wcel 2105 〈cop 4563 ◡ccnv 5547 Rel wrel 5553 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-xp 5554 df-rel 5555 df-cnv 5556 |
This theorem is referenced by: dfrel4v 6040 cnvcnv 6042 cnveqb 6046 dfrel3 6048 cnvcnvres 6055 cnvsng 6073 cores2 6105 co01 6107 coi2 6109 relcnvtrg 6112 funcnvres2 6427 f1cnvcnv 6577 f1ocnv 6620 f1ocnvb 6621 f1ococnv1 6636 fimacnvinrn 6832 isores1 7076 relcnvexb 7620 cnvf1o 7795 fnwelem 7814 tposf12 7906 ssenen 8679 cantnffval2 9146 fsumcnv 15116 fprodcnv 15325 structcnvcnv 16485 imasless 16801 oppcinv 17038 cnvps 17810 cnvpsb 17811 cnvtsr 17820 gimcnv 18345 lmimcnv 19768 hmeocnv 22298 hmeocnvb 22310 cmphaushmeo 22336 ustexsym 22751 pi1xfrcnv 23588 dvlog 25161 efopnlem2 25167 gtiso 30362 cycpmconjvlem 30710 cycpmconjs 30725 f1ocan2fv 34883 relcnveq3 35459 relcnveq2 35461 brcnvrabga 35480 dfrel5 35484 elrelscnveq3 35611 elrelscnveq2 35613 ltrncnvnid 37143 relintab 39821 cnvssb 39824 relnonrel 39825 cononrel1 39832 cononrel2 39833 clrellem 39860 clcnvlem 39861 relexpaddss 39941 |
Copyright terms: Public domain | W3C validator |