Theorem dfrel2 6081

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 6001	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3426	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3426	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5779	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5779	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 274	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5688	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 686	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5677	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 232	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 208	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ⟨cop 4564  ^◡ccnv 5579  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588

This theorem is referenced by:  dfrel4v  6082  cnvcnv  6084  cnveqb  6088  dfrel3  6090  cnvcnvres  6097  cnvsng  6115  cores2  6152  co01  6154  coi2  6156  relcnvtrg  6159  funcnvres2  6498  f1cnvcnv  6664  f1ocnv  6712  f1ocnvb  6713  f1ococnv1  6728  fimacnvinrn  6931  isores1  7185  relcnvexb  7747  cnvf1o  7922  fnwelem  7943  tposf12  8038  ssenen  8887  f1oenfirn  8927  f1domfi  8928  cantnffval2  9383  fsumcnv  15413  fprodcnv  15621  structcnvcnv  16782  imasless  17168  oppcinv  17409  cnvps  18211  cnvpsb  18212  cnvtsr  18221  gimcnv  18798  lmimcnv  20244  hmeocnv  22821  hmeocnvb  22833  cmphaushmeo  22859  ustexsym  23275  pi1xfrcnv  24126  dvlog  25711  efopnlem2  25717  gtiso  30935  cycpmconjvlem  31310  cycpmconjs  31325  f1ocan2fv  35812  relcnveq3  36383  relcnveq2  36385  brcnvrabga  36404  dfrel5  36408  elrelscnveq3  36536  elrelscnveq2  36538  ltrncnvnid  38068  relintab  41080  cnvssb  41083  relnonrel  41084  cononrel1  41091  cononrel2  41092  clrellem  41119  clcnvlem  41120  relexpaddss  41215