![]() |
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 6092 | . . 3 ⊢ Rel ◡◡𝑅 | |
2 | vex 3477 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | vex 3477 | . . . . . 6 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opelcnv 5873 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝑅) |
5 | 3, 2 | opelcnv 5873 | . . . . 5 ⊢ (〈𝑦, 𝑥〉 ∈ ◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
6 | 4, 5 | bitri 274 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ◡◡𝑅 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
7 | 6 | eqrelriv 5781 | . . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅) |
8 | 1, 7 | mpan 688 | . 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅) |
9 | releq 5768 | . . 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 1541 ∈ wcel 2106 〈cop 4628 ◡ccnv 5668 Rel wrel 5674 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-xp 5675 df-rel 5676 df-cnv 5677 |
This theorem is referenced by: dfrel4v 6178 cnvcnv 6180 cnveqb 6184 dfrel3 6186 cnvcnvres 6193 cnvsng 6211 cores2 6247 co01 6249 coi2 6251 relcnvtrg 6254 funcnvres2 6617 f1cnvcnv 6784 f1ocnv 6832 f1ocnvb 6833 f1ococnv1 6849 fimacnvinrn 7058 isores1 7315 relcnvexb 7899 cnvf1o 8079 fnwelem 8099 tposf12 8218 ssenen 9134 f1oenfirn 9166 f1domfi 9167 cantnffval2 9672 fsumcnv 15701 fprodcnv 15909 structcnvcnv 17068 imasless 17468 oppcinv 17709 cnvps 18513 cnvpsb 18514 cnvtsr 18523 gimcnv 19107 lmimcnv 20627 hmeocnv 23195 hmeocnvb 23207 cmphaushmeo 23233 ustexsym 23649 pi1xfrcnv 24502 dvlog 26088 efopnlem2 26094 gtiso 31793 cycpmconjvlem 32171 cycpmconjs 32186 f1ocan2fv 36400 relcnveq3 36995 relcnveq2 36997 brcnvrabga 37016 dfrel5 37020 elrelscnveq3 37166 elrelscnveq2 37168 ltrncnvnid 38803 rimcnv 40896 relintab 42105 cnvssb 42108 relnonrel 42109 cononrel1 42116 cononrel2 42117 clrellem 42144 clcnvlem 42145 relexpaddss 42240 |
Copyright terms: Public domain | W3C validator |