Theorem dfrel2 6178

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 6091	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3463	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3463	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5861	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5861	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5768	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 690	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5755	. . 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 4607  ^◡ccnv 5653  Rel wrel 5659

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662

This theorem is referenced by:  dfrel4v  6179  cnvcnv  6181  cnveqb  6185  dfrel3  6187  cnvcnvres  6194  cnvsng  6212  cores2  6248  co01  6250  coi2  6252  relcnvtrg  6255  funcnvres2  6616  f1cnvcnv  6783  f1ocnv  6830  f1ocnvb  6831  f1ococnv1  6847  fimacnvinrn  7061  isores1  7327  relcnvexb  7922  cnvf1o  8110  fnwelem  8130  tposf12  8250  ssenen  9165  f1oenfirn  9194  f1domfi  9195  cantnffval2  9709  fsumcnv  15789  fprodcnv  15999  structcnvcnv  17172  imasless  17554  oppcinv  17793  cnvps  18588  cnvpsb  18589  cnvtsr  18598  gimcnv  19250  rngimcnv  20416  lmimcnv  21025  hmeocnv  23700  hmeocnvb  23712  cmphaushmeo  23738  ustexsym  24154  pi1xfrcnv  25008  dvlog  26612  efopnlem2  26618  gtiso  32678  cycpmconjvlem  33152  cycpmconjs  33167  f1ocan2fv  37751  relcnveq3  38339  relcnveq2  38341  brcnvrabga  38360  dfrel5  38364  elrelscnveq3  38509  elrelscnveq2  38511  ltrncnvnid  40146  rimcnv  42540  relintab  43607  cnvssb  43610  relnonrel  43611  cononrel1  43618  cononrel2  43619  clrellem  43646  clcnvlem  43647  relexpaddss  43742  3f1oss1  47104  3f1oss2  47105  tposideq  48863