Theorem dfrel2 6187

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2104  ⟨cop 4633  ^◡ccnv 5674  Rel wrel 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683

This theorem is referenced by:  dfrel4v  6188  cnvcnv  6190  cnveqb  6194  dfrel3  6196  cnvcnvres  6203  cnvsng  6221  cores2  6257  co01  6259  coi2  6261  relcnvtrg  6264  funcnvres2  6627  f1cnvcnv  6796  f1ocnv  6844  f1ocnvb  6845  f1ococnv1  6861  fimacnvinrn  7072  isores1  7333  relcnvexb  7919  cnvf1o  8099  fnwelem  8119  tposf12  8238  ssenen  9153  f1oenfirn  9185  f1domfi  9186  cantnffval2  9692  fsumcnv  15723  fprodcnv  15931  structcnvcnv  17090  imasless  17490  oppcinv  17731  cnvps  18535  cnvpsb  18536  cnvtsr  18545  gimcnv  19181  rngimcnv  20347  lmimcnv  20822  hmeocnv  23486  hmeocnvb  23498  cmphaushmeo  23524  ustexsym  23940  pi1xfrcnv  24804  dvlog  26395  efopnlem2  26401  gtiso  32189  cycpmconjvlem  32570  cycpmconjs  32585  f1ocan2fv  36898  relcnveq3  37493  relcnveq2  37495  brcnvrabga  37514  dfrel5  37518  elrelscnveq3  37664  elrelscnveq2  37666  ltrncnvnid  39301  rimcnv  41396  relintab  42636  cnvssb  42639  relnonrel  42640  cononrel1  42647  cononrel2  42648  clrellem  42675  clcnvlem  42676  relexpaddss  42771