Theorem dfrel2 6220

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 6134	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3492	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3492	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5906	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5906	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5813	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 689	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5800	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 233	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 209	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ⟨cop 4654  ^◡ccnv 5699  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708

This theorem is referenced by:  dfrel4v  6221  cnvcnv  6223  cnveqb  6227  dfrel3  6229  cnvcnvres  6236  cnvsng  6254  cores2  6290  co01  6292  coi2  6294  relcnvtrg  6297  funcnvres2  6658  f1cnvcnv  6826  f1ocnv  6874  f1ocnvb  6875  f1ococnv1  6891  fimacnvinrn  7105  isores1  7370  relcnvexb  7966  cnvf1o  8152  fnwelem  8172  tposf12  8292  ssenen  9217  f1oenfirn  9246  f1domfi  9247  cantnffval2  9764  fsumcnv  15821  fprodcnv  16031  structcnvcnv  17200  imasless  17600  oppcinv  17841  cnvps  18648  cnvpsb  18649  cnvtsr  18658  gimcnv  19307  rngimcnv  20482  lmimcnv  21089  hmeocnv  23791  hmeocnvb  23803  cmphaushmeo  23829  ustexsym  24245  pi1xfrcnv  25109  dvlog  26711  efopnlem2  26717  gtiso  32712  cycpmconjvlem  33134  cycpmconjs  33149  f1ocan2fv  37687  relcnveq3  38277  relcnveq2  38279  brcnvrabga  38298  dfrel5  38302  elrelscnveq3  38447  elrelscnveq2  38449  ltrncnvnid  40084  rimcnv  42472  relintab  43545  cnvssb  43548  relnonrel  43549  cononrel1  43556  cononrel2  43557  clrellem  43584  clcnvlem  43585  relexpaddss  43680  3f1oss1  46990  3f1oss2  46991