Theorem dfrel2 6148

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 6064	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3445	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3445	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5831	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5831	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5739	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 691	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5727	. . 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 4587  ^◡ccnv 5624  Rel wrel 5630

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 5242  ax-nul 5252  ax-pr 5378

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-rel 5632  df-cnv 5633

This theorem is referenced by:  dfrel4v  6149  cnvcnv  6151  cnveqb  6155  dfrel3  6157  cnvcnvres  6164  cnvsng  6182  cores2  6219  co01  6221  coi2  6223  relcnvtrg  6226  funcnvres2  6573  f1cnvcnv  6740  f1ocnv  6787  f1ocnvb  6788  f1ococnv1  6804  fimacnvinrn  7018  isores1  7282  relcnvexb  7870  cnvf1o  8055  fnwelem  8075  tposf12  8195  ssenen  9083  f1oenfirn  9108  f1domfi  9109  cantnffval2  9608  fsumcnv  15700  fprodcnv  15910  structcnvcnv  17084  imasless  17465  oppcinv  17708  cnvps  18505  cnvpsb  18506  cnvtsr  18515  gimcnv  19200  rngimcnv  20396  lmimcnv  21023  hmeocnv  23710  hmeocnvb  23722  cmphaushmeo  23748  ustexsym  24164  pi1xfrcnv  25017  dvlog  26620  efopnlem2  26626  gtiso  32761  cycpmconjvlem  33204  cycpmconjs  33219  f1ocan2fv  37899  relcnveq3  38499  relcnveq2  38501  brcnvrabga  38514  dfrel5  38518  elrelscnveq3  38799  elrelscnveq2  38801  ltrncnvnid  40424  rimcnv  42808  relintab  43860  cnvssb  43863  relnonrel  43864  cononrel1  43871  cononrel2  43872  clrellem  43899  clcnvlem  43900  relexpaddss  43995  3f1oss1  47357  3f1oss2  47358  tposideq  49169