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 6012 | . . 3 ⊢ Rel ◡◡𝑅 | |
2 | vex 3436 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | vex 3436 | . . . . . 6 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opelcnv 5790 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝑅) |
5 | 3, 2 | opelcnv 5790 | . . . . 5 ⊢ (〈𝑦, 𝑥〉 ∈ ◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
6 | 4, 5 | bitri 274 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
7 | 6 | eqrelriv 5699 | . . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅) |
8 | 1, 7 | mpan 687 | . 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅) |
9 | releq 5687 | . . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅)) | |
10 | 1, 9 | mpbii 232 | . 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅) |
11 | 8, 10 | impbii 208 | 1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 ∈ wcel 2106 〈cop 4567 ◡ccnv 5588 Rel wrel 5594 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-rel 5596 df-cnv 5597 |
This theorem is referenced by: dfrel4v 6093 cnvcnv 6095 cnveqb 6099 dfrel3 6101 cnvcnvres 6108 cnvsng 6126 cores2 6163 co01 6165 coi2 6167 relcnvtrg 6170 funcnvres2 6514 f1cnvcnv 6680 f1ocnv 6728 f1ocnvb 6729 f1ococnv1 6745 fimacnvinrn 6949 isores1 7205 relcnvexb 7773 cnvf1o 7951 fnwelem 7972 tposf12 8067 ssenen 8938 f1oenfirn 8966 f1domfi 8967 cantnffval2 9453 fsumcnv 15485 fprodcnv 15693 structcnvcnv 16854 imasless 17251 oppcinv 17492 cnvps 18296 cnvpsb 18297 cnvtsr 18306 gimcnv 18883 lmimcnv 20329 hmeocnv 22913 hmeocnvb 22925 cmphaushmeo 22951 ustexsym 23367 pi1xfrcnv 24220 dvlog 25806 efopnlem2 25812 gtiso 31033 cycpmconjvlem 31408 cycpmconjs 31423 f1ocan2fv 35885 relcnveq3 36456 relcnveq2 36458 brcnvrabga 36477 dfrel5 36481 elrelscnveq3 36609 elrelscnveq2 36611 ltrncnvnid 38141 relintab 41191 cnvssb 41194 relnonrel 41195 cononrel1 41202 cononrel2 41203 clrellem 41230 clcnvlem 41231 relexpaddss 41326 |
Copyright terms: Public domain | W3C validator |