Theorem dfrel2 6147

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 6063	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3434	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3434	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5830	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5830	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5738	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 691	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5726	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 233	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 209	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ⟨cop 4574  ^◡ccnv 5623  Rel wrel 5629

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632

This theorem is referenced by:  dfrel4v  6148  cnvcnv  6150  cnveqb  6154  dfrel3  6156  cnvcnvres  6163  cnvsng  6181  cores2  6218  co01  6220  coi2  6222  relcnvtrg  6225  funcnvres2  6572  f1cnvcnv  6739  f1ocnv  6786  f1ocnvb  6787  f1ococnv1  6803  fimacnvinrn  7017  isores1  7282  relcnvexb  7870  cnvf1o  8054  fnwelem  8074  tposf12  8194  ssenen  9082  f1oenfirn  9107  f1domfi  9108  cantnffval2  9607  fsumcnv  15726  fprodcnv  15939  structcnvcnv  17114  imasless  17495  oppcinv  17738  cnvps  18535  cnvpsb  18536  cnvtsr  18545  gimcnv  19233  rngimcnv  20427  lmimcnv  21054  hmeocnv  23737  hmeocnvb  23749  cmphaushmeo  23775  ustexsym  24191  pi1xfrcnv  25034  dvlog  26628  efopnlem2  26634  gtiso  32789  cycpmconjvlem  33217  cycpmconjs  33232  f1ocan2fv  38062  relcnveq3  38662  relcnveq2  38664  brcnvrabga  38677  dfrel5  38681  elrelscnveq3  38962  elrelscnveq2  38964  ltrncnvnid  40587  rimcnv  42976  relintab  44028  cnvssb  44031  relnonrel  44032  cononrel1  44039  cononrel2  44040  clrellem  44067  clcnvlem  44068  relexpaddss  44163  3f1oss1  47535  3f1oss2  47536  tposideq  49375