Theorem dfrel2 6092

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 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 𝑅 ↔ ◡◡𝑅 = 𝑅)

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