Theorem dfrel2 6169

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 6088	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3457	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3457	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5849	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5849	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 277	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5757	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 700	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5745	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 235	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 211	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ⟨cop 4585  ^◡ccnv 5642  Rel wrel 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651

This theorem is referenced by:  dfrel4v  6170  cnvcnv  6172  cnveqb  6177  dfrel3  6179  cnvcnvres  6186  cnvsng  6204  cores2  6241  co01  6243  coi2  6245  relcnvtrg  6248  funcnvres2  6595  f1cnvcnv  6765  f1ocnv  6813  f1ocnvb  6814  f1ococnv1  6830  fimacnvinrn  7046  isores1  7312  relcnvexb  7901  cnvf1o  8083  fnwelem  8104  tposf12  8224  ssenen  9116  f1oenfirn  9141  f1domfi  9142  cantnffval2  9643  fsumcnv  15790  fprodcnv  16003  structcnvcnv  17179  imasless  17560  oppcinv  17803  cnvps  18600  cnvpsb  18601  cnvtsr  18610  gimcnv  19297  rngimcnv  20491  rimcnv  20520  lmimcnv  21121  hmeocnv  23809  hmeocnvb  23821  cmphaushmeo  23847  ustexsym  24263  pi1xfrcnv  25106  dvlog  26703  efopnlem2  26709  gtiso  32863  cycpmconjvlem  33281  cycpmconjs  33296  f1ocan2fv  38186  relcnveq3  38786  relcnveq2  38788  brcnvrabga  38801  dfrel5  38805  elrelscnveq3  39086  elrelscnveq2  39088  ltrncnvnid  40711  relintab  44119  cnvssb  44122  relnonrel  44123  cononrel1  44130  cononrel2  44131  clrellem  44158  clcnvlem  44159  relexpaddss  44254  3f1oss1  47629  3f1oss2  47630  tposideq  49469