dfrel2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dfrel2		Structured version Visualization version GIF version

Theorem dfrel2 5502

Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)

**Assertion**
Ref	Expression
dfrel2	⊢ (Rel 𝑅 ↔ ^◡^◡𝑅 = 𝑅)

Proof of Theorem dfrel2 Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relcnv 5422	. . 3 ⊢ Rel ^◡^◡𝑅
2		vex 3176	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3176	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5226	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ^◡^◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
5	3, 2	opelcnv 5226	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 263	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ^◡^◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5136	. . 3 ⊢ ((Rel ^◡^◡𝑅 ∧ Rel 𝑅) → ^◡^◡𝑅 = 𝑅)
8	1, 7	mpan 702	. 2 ⊢ (Rel 𝑅 → ^◡^◡𝑅 = 𝑅)
9		releq 5124	. . 3 ⊢ (^◡^◡𝑅 = 𝑅 → (Rel ^◡^◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 222	. 2 ⊢ (^◡^◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 198	1 ⊢ (Rel 𝑅 ↔ ^◡^◡𝑅 = 𝑅)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 ⟨cop 4131 ^◡ccnv 5037 Rel wrel 5043

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-cnv 5046

This theorem is referenced by: dfrel4v 5503 cnvcnv 5505 cnveqb 5508 dfrel3 5510 cnvcnvres 5516 cnvsn 5536 cores2 5565 co01 5567 coi2 5569 relcnvtr 5572 funcnvres2 5883 f1cnvcnv 6022 f1ocnv 6062 f1ocnvb 6063 f1ococnv1 6078 fimacnvinrn 6256 isores1 6484 relcnvexb 7007 cnvf1o 7163 fnwelem 7179 tposf12 7264 ssenen 8019 cantnffval2 8475 fsumcnv 14346 fprodcnv 14552 structcnvcnv 15706 imasless 16023 oppcinv 16263 cnvps 17035 cnvpsb 17036 cnvtsr 17045 gimcnv 17532 lmimcnv 18888 hmeocnv 21375 hmeocnvb 21387 cmphaushmeo 21413 ustexsym 21829 pi1xfrcnv 22665 dvlog 24197 efopnlem2 24203 gtiso 28861 f1ocan2fv 32692 ltrncnvnid 34431 relintab 36908 cnvssb 36911 relnonrel 36912 cononrel1 36919 cononrel2 36920 clrellem 36948 clcnvlem 36949 relexpaddss 37029