Theorem dfrel2 6147

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ⟨cop 4586  ^◡ccnv 5623  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632

This theorem is referenced by:  dfrel4v  6148  cnvcnv  6150  cnveqb  6154  dfrel3  6156  cnvcnvres  6163  cnvsng  6181  cores2  6218  co01  6220  coi2  6222  relcnvtrg  6225  funcnvres2  6572  f1cnvcnv  6739  f1ocnv  6786  f1ocnvb  6787  f1ococnv1  6803  fimacnvinrn  7016  isores1  7280  relcnvexb  7868  cnvf1o  8053  fnwelem  8073  tposf12  8193  ssenen  9079  f1oenfirn  9104  f1domfi  9105  cantnffval2  9604  fsumcnv  15696  fprodcnv  15906  structcnvcnv  17080  imasless  17461  oppcinv  17704  cnvps  18501  cnvpsb  18502  cnvtsr  18511  gimcnv  19196  rngimcnv  20392  lmimcnv  21019  hmeocnv  23706  hmeocnvb  23718  cmphaushmeo  23744  ustexsym  24160  pi1xfrcnv  25013  dvlog  26616  efopnlem2  26622  gtiso  32780  cycpmconjvlem  33223  cycpmconjs  33238  f1ocan2fv  37924  relcnveq3  38516  relcnveq2  38518  brcnvrabga  38531  dfrel5  38535  elrelscnveq3  38796  elrelscnveq2  38798  ltrncnvnid  40383  rimcnv  42768  relintab  43820  cnvssb  43823  relnonrel  43824  cononrel1  43831  cononrel2  43832  clrellem  43859  clcnvlem  43860  relexpaddss  43955  3f1oss1  47317  3f1oss2  47318  tposideq  49129