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 5941 | . . 3 ⊢ Rel ◡◡𝑅 | |
2 | vex 3402 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | vex 3402 | . . . . . 6 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opelcnv 5724 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝑅) |
5 | 3, 2 | opelcnv 5724 | . . . . 5 ⊢ (〈𝑦, 𝑥〉 ∈ ◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
6 | 4, 5 | bitri 278 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
7 | 6 | eqrelriv 5633 | . . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅) |
8 | 1, 7 | mpan 690 | . 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅) |
9 | releq 5622 | . . 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 1542 ∈ wcel 2114 〈cop 4522 ◡ccnv 5524 Rel wrel 5530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-br 5031 df-opab 5093 df-xp 5531 df-rel 5532 df-cnv 5533 |
This theorem is referenced by: dfrel4v 6022 cnvcnv 6024 cnveqb 6028 dfrel3 6030 cnvcnvres 6037 cnvsng 6055 cores2 6092 co01 6094 coi2 6096 relcnvtrg 6099 funcnvres2 6419 f1cnvcnv 6584 f1ocnv 6630 f1ocnvb 6631 f1ococnv1 6646 fimacnvinrn 6849 isores1 7100 relcnvexb 7657 cnvf1o 7832 fnwelem 7851 tposf12 7946 ssenen 8741 f1oenfirn 8780 cantnffval2 9231 fsumcnv 15221 fprodcnv 15429 structcnvcnv 16600 imasless 16916 oppcinv 17155 cnvps 17938 cnvpsb 17939 cnvtsr 17948 gimcnv 18525 lmimcnv 19958 hmeocnv 22513 hmeocnvb 22525 cmphaushmeo 22551 ustexsym 22967 pi1xfrcnv 23809 dvlog 25394 efopnlem2 25400 gtiso 30608 cycpmconjvlem 30985 cycpmconjs 31000 f1ocan2fv 35528 relcnveq3 36099 relcnveq2 36101 brcnvrabga 36120 dfrel5 36124 elrelscnveq3 36252 elrelscnveq2 36254 ltrncnvnid 37784 relintab 40756 cnvssb 40759 relnonrel 40760 cononrel1 40767 cononrel2 40768 clrellem 40795 clcnvlem 40796 relexpaddss 40892 |
Copyright terms: Public domain | W3C validator |