Theorem dfrel2 6165

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 6078	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5848	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5848	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5755	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 690	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5742	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 233	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 209	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ⟨cop 4598  ^◡ccnv 5640  Rel wrel 5646

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649

This theorem is referenced by:  dfrel4v  6166  cnvcnv  6168  cnveqb  6172  dfrel3  6174  cnvcnvres  6181  cnvsng  6199  cores2  6235  co01  6237  coi2  6239  relcnvtrg  6242  funcnvres2  6599  f1cnvcnv  6768  f1ocnv  6815  f1ocnvb  6816  f1ococnv1  6832  fimacnvinrn  7046  isores1  7312  relcnvexb  7905  cnvf1o  8093  fnwelem  8113  tposf12  8233  ssenen  9121  f1oenfirn  9150  f1domfi  9151  cantnffval2  9655  fsumcnv  15746  fprodcnv  15956  structcnvcnv  17130  imasless  17510  oppcinv  17749  cnvps  18544  cnvpsb  18545  cnvtsr  18554  gimcnv  19206  rngimcnv  20372  lmimcnv  20981  hmeocnv  23656  hmeocnvb  23668  cmphaushmeo  23694  ustexsym  24110  pi1xfrcnv  24964  dvlog  26567  efopnlem2  26573  gtiso  32631  cycpmconjvlem  33105  cycpmconjs  33120  f1ocan2fv  37728  relcnveq3  38316  relcnveq2  38318  brcnvrabga  38331  dfrel5  38335  elrelscnveq3  38489  elrelscnveq2  38491  ltrncnvnid  40128  rimcnv  42512  relintab  43579  cnvssb  43582  relnonrel  43583  cononrel1  43590  cononrel2  43591  clrellem  43618  clcnvlem  43619  relexpaddss  43714  3f1oss1  47080  3f1oss2  47081  tposideq  48880