Theorem dfrel2 6189

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 6108	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3459	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3459	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5869	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5869	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5777	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 702	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5765	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 236	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 212	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ⟨cop 4596  ^◡ccnv 5662  Rel wrel 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671

This theorem is referenced by:  dfrel4v  6190  cnvcnv  6192  cnveqb  6197  dfrel3  6199  cnvcnvres  6208  cnvsng  6226  cores2  6263  co01  6265  coi2  6267  relcnvtrg  6270  funcnvres2  6618  f1cnvcnv  6787  f1ocnv  6835  f1ocnvb  6836  f1ococnv1  6852  fimacnvinrn  7068  isores1  7334  relcnvexb  7924  cnvf1o  8107  fnwelem  8128  tposf12  8248  ssenen  9140  f1oenfirn  9165  f1domfi  9166  cantnffval2  9665  fsumcnv  15826  fprodcnv  16039  structcnvcnv  17214  imasless  17595  oppcinv  17838  cnvps  18635  cnvpsb  18636  cnvtsr  18645  gimcnv  19338  rngimcnv  20539  rimcnv  20568  lmimcnv  21169  hmeocnv  23900  hmeocnvb  23912  cmphaushmeo  23938  ustexsym  24354  pi1xfrcnv  25197  dvlog  26797  efopnlem2  26803  gtiso  33027  cycpmconjvlem  33442  cycpmconjs  33457  f1ocan2fv  38359  relcnveq3  38957  relcnveq2  38959  brcnvrabga  38972  dfrel5  38976  elrelscnveq3  39257  elrelscnveq2  39259  ltrncnvnid  40882  relintab  44292  cnvssb  44295  relnonrel  44296  cononrel1  44303  cononrel2  44304  clrellem  44331  clcnvlem  44332  relexpaddss  44427  3f1oss1  47795  3f1oss2  47796  tposideq  49649