Theorem dfrel2 6185

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 6100	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3479	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3479	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5879	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5879	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5787	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 689	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5774	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 232	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 208	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ⟨cop 4633  ^◡ccnv 5674  Rel wrel 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683

This theorem is referenced by:  dfrel4v  6186  cnvcnv  6188  cnveqb  6192  dfrel3  6194  cnvcnvres  6201  cnvsng  6219  cores2  6255  co01  6257  coi2  6259  relcnvtrg  6262  funcnvres2  6625  f1cnvcnv  6794  f1ocnv  6842  f1ocnvb  6843  f1ococnv1  6859  fimacnvinrn  7069  isores1  7326  relcnvexb  7912  cnvf1o  8092  fnwelem  8112  tposf12  8231  ssenen  9147  f1oenfirn  9179  f1domfi  9180  cantnffval2  9686  fsumcnv  15715  fprodcnv  15923  structcnvcnv  17082  imasless  17482  oppcinv  17723  cnvps  18527  cnvpsb  18528  cnvtsr  18537  gimcnv  19135  lmimcnv  20666  hmeocnv  23248  hmeocnvb  23260  cmphaushmeo  23286  ustexsym  23702  pi1xfrcnv  24555  dvlog  26141  efopnlem2  26147  gtiso  31900  cycpmconjvlem  32278  cycpmconjs  32293  f1ocan2fv  36533  relcnveq3  37128  relcnveq2  37130  brcnvrabga  37149  dfrel5  37153  elrelscnveq3  37299  elrelscnveq2  37301  ltrncnvnid  38936  rimcnv  41041  relintab  42267  cnvssb  42270  relnonrel  42271  cononrel1  42278  cononrel2  42279  clrellem  42306  clcnvlem  42307  relexpaddss  42402  rngimcnv  46639