Theorem dfrel2 6209

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 6122	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3484	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3484	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5892	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5892	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5799	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 690	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5786	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 233	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 209	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ⟨cop 4632  ^◡ccnv 5684  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693

This theorem is referenced by:  dfrel4v  6210  cnvcnv  6212  cnveqb  6216  dfrel3  6218  cnvcnvres  6225  cnvsng  6243  cores2  6279  co01  6281  coi2  6283  relcnvtrg  6286  funcnvres2  6646  f1cnvcnv  6813  f1ocnv  6860  f1ocnvb  6861  f1ococnv1  6877  fimacnvinrn  7091  isores1  7354  relcnvexb  7948  cnvf1o  8136  fnwelem  8156  tposf12  8276  ssenen  9191  f1oenfirn  9220  f1domfi  9221  cantnffval2  9735  fsumcnv  15809  fprodcnv  16019  structcnvcnv  17190  imasless  17585  oppcinv  17824  cnvps  18623  cnvpsb  18624  cnvtsr  18633  gimcnv  19285  rngimcnv  20456  lmimcnv  21066  hmeocnv  23770  hmeocnvb  23782  cmphaushmeo  23808  ustexsym  24224  pi1xfrcnv  25090  dvlog  26693  efopnlem2  26699  gtiso  32710  cycpmconjvlem  33161  cycpmconjs  33176  f1ocan2fv  37734  relcnveq3  38322  relcnveq2  38324  brcnvrabga  38343  dfrel5  38347  elrelscnveq3  38492  elrelscnveq2  38494  ltrncnvnid  40129  rimcnv  42527  relintab  43596  cnvssb  43599  relnonrel  43600  cononrel1  43607  cononrel2  43608  clrellem  43635  clcnvlem  43636  relexpaddss  43731  3f1oss1  47087  3f1oss2  47088  tposideq  48788