Theorem dfrel2 6021

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 5941	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3402	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3402	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5724	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5724	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5633	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 690	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5622	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 236	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 212	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 209   = wceq 1542   ∈ wcel 2114  ⟨cop 4522  ^◡ccnv 5524  Rel wrel 5530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-xp 5531  df-rel 5532  df-cnv 5533

This theorem is referenced by:  dfrel4v  6022  cnvcnv  6024  cnveqb  6028  dfrel3  6030  cnvcnvres  6037  cnvsng  6055  cores2  6092  co01  6094  coi2  6096  relcnvtrg  6099  funcnvres2  6419  f1cnvcnv  6584  f1ocnv  6630  f1ocnvb  6631  f1ococnv1  6646  fimacnvinrn  6849  isores1  7100  relcnvexb  7657  cnvf1o  7832  fnwelem  7851  tposf12  7946  ssenen  8741  f1oenfirn  8780  cantnffval2  9231  fsumcnv  15221  fprodcnv  15429  structcnvcnv  16600  imasless  16916  oppcinv  17155  cnvps  17938  cnvpsb  17939  cnvtsr  17948  gimcnv  18525  lmimcnv  19958  hmeocnv  22513  hmeocnvb  22525  cmphaushmeo  22551  ustexsym  22967  pi1xfrcnv  23809  dvlog  25394  efopnlem2  25400  gtiso  30608  cycpmconjvlem  30985  cycpmconjs  31000  f1ocan2fv  35528  relcnveq3  36099  relcnveq2  36101  brcnvrabga  36120  dfrel5  36124  elrelscnveq3  36252  elrelscnveq2  36254  ltrncnvnid  37784  relintab  40756  cnvssb  40759  relnonrel  40760  cononrel1  40767  cononrel2  40768  clrellem  40795  clcnvlem  40796  relexpaddss  40892