Theorem dfrel2 6155

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 6071	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3446	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3446	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5838	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5838	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5746	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 691	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5734	. . 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 4588  ^◡ccnv 5631  Rel wrel 5637

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640

This theorem is referenced by:  dfrel4v  6156  cnvcnv  6158  cnveqb  6162  dfrel3  6164  cnvcnvres  6171  cnvsng  6189  cores2  6226  co01  6228  coi2  6230  relcnvtrg  6233  funcnvres2  6580  f1cnvcnv  6747  f1ocnv  6794  f1ocnvb  6795  f1ococnv1  6811  fimacnvinrn  7025  isores1  7290  relcnvexb  7878  cnvf1o  8063  fnwelem  8083  tposf12  8203  ssenen  9091  f1oenfirn  9116  f1domfi  9117  cantnffval2  9616  fsumcnv  15708  fprodcnv  15918  structcnvcnv  17092  imasless  17473  oppcinv  17716  cnvps  18513  cnvpsb  18514  cnvtsr  18523  gimcnv  19208  rngimcnv  20404  lmimcnv  21031  hmeocnv  23718  hmeocnvb  23730  cmphaushmeo  23756  ustexsym  24172  pi1xfrcnv  25025  dvlog  26628  efopnlem2  26634  gtiso  32790  cycpmconjvlem  33234  cycpmconjs  33249  f1ocan2fv  37975  relcnveq3  38575  relcnveq2  38577  brcnvrabga  38590  dfrel5  38594  elrelscnveq3  38875  elrelscnveq2  38877  ltrncnvnid  40500  rimcnv  42884  relintab  43936  cnvssb  43939  relnonrel  43940  cononrel1  43947  cononrel2  43948  clrellem  43975  clcnvlem  43976  relexpaddss  44071  3f1oss1  47432  3f1oss2  47433  tposideq  49244