Theorem dfrel2 6211

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2106  ⟨cop 4637  ^◡ccnv 5688  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697

This theorem is referenced by:  dfrel4v  6212  cnvcnv  6214  cnveqb  6218  dfrel3  6220  cnvcnvres  6227  cnvsng  6245  cores2  6281  co01  6283  coi2  6285  relcnvtrg  6288  funcnvres2  6648  f1cnvcnv  6814  f1ocnv  6861  f1ocnvb  6862  f1ococnv1  6878  fimacnvinrn  7091  isores1  7354  relcnvexb  7949  cnvf1o  8135  fnwelem  8155  tposf12  8275  ssenen  9190  f1oenfirn  9218  f1domfi  9219  cantnffval2  9733  fsumcnv  15806  fprodcnv  16016  structcnvcnv  17187  imasless  17587  oppcinv  17828  cnvps  18636  cnvpsb  18637  cnvtsr  18646  gimcnv  19298  rngimcnv  20473  lmimcnv  21084  hmeocnv  23786  hmeocnvb  23798  cmphaushmeo  23824  ustexsym  24240  pi1xfrcnv  25104  dvlog  26708  efopnlem2  26714  gtiso  32716  cycpmconjvlem  33144  cycpmconjs  33159  f1ocan2fv  37714  relcnveq3  38303  relcnveq2  38305  brcnvrabga  38324  dfrel5  38328  elrelscnveq3  38473  elrelscnveq2  38475  ltrncnvnid  40110  rimcnv  42504  relintab  43573  cnvssb  43576  relnonrel  43577  cononrel1  43584  cononrel2  43585  clrellem  43612  clcnvlem  43613  relexpaddss  43708  3f1oss1  47025  3f1oss2  47026