Theorem dfrel2 5823

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 5743	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3416	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3416	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5535	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5535	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 267	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5446	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 683	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5435	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 225	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 201	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 198   = wceq 1658   ∈ wcel 2166  ⟨cop 4402  ^◡ccnv 5340  Rel wrel 5346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pr 5126

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-br 4873  df-opab 4935  df-xp 5347  df-rel 5348  df-cnv 5349

This theorem is referenced by:  dfrel4v  5824  cnvcnv  5826  cnveqb  5829  dfrel3  5831  cnvcnvres  5838  cnvsng  5856  cores2  5888  co01  5890  coi2  5892  relcnvtr  5895  funcnvres2  6201  f1cnvcnv  6346  f1ocnv  6389  f1ocnvb  6390  f1ococnv1  6405  fimacnvinrn  6596  isores1  6838  relcnvexb  7375  cnvf1o  7539  fnwelem  7555  tposf12  7641  ssenen  8402  cantnffval2  8868  fsumcnv  14878  fprodcnv  15085  structcnvcnv  16235  imasless  16552  oppcinv  16791  cnvps  17564  cnvpsb  17565  cnvtsr  17574  gimcnv  18059  lmimcnv  19425  hmeocnv  21935  hmeocnvb  21947  cmphaushmeo  21973  ustexsym  22388  pi1xfrcnv  23225  dvlog  24795  efopnlem2  24801  gtiso  30025  f1ocan2fv  34064  relcnveq3  34639  relcnveq2  34641  brcnvrabga  34657  dfrel5  34661  elrelscnveq3  34788  elrelscnveq2  34790  ltrncnvnid  36201  relintab  38729  cnvssb  38732  relnonrel  38733  cononrel1  38740  cononrel2  38741  clrellem  38769  clcnvlem  38770  relexpaddss  38850