Theorem dfrel2 6180

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 6099	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5858	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5858	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5764	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 703	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5752	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 236	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 212	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ⟨cop 4834  ^◡ccnv 5649  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658

This theorem is used by:  dfrel4v  6181  cnvcnv  6183  cnvssb  6188  dfrel3  6192  cnvcnvres  6206  cnvsng  6224  cores2  6261  co01  6263  coi2  6265  relcnvtrgOLD  6269  funcnvres2  6620  f1cnvcnv  6789  f1ocnv  6837  f1ocnvb  6838  f1ococnv1  6854  fimacnvinrn  7071  isores1  7342  relcnvexb  7938  cnvf1o  8124  fnwelem  8145  tposf12  8271  ssenen  9173  f1oenfirn  9198  f1domfi  9199  cantnffval2  9699  fsumcnv  15944  fprodcnv  16155  structcnvcnv  17336  imasless  17717  oppcinv  17960  cnvps  18757  cnvpsb  18758  cnvtsr  18767  gimcnv  19486  rngimcnv  20691  rimcnv  20722  lmimcnv  21347  hmeocnv  24086  hmeocnvb  24098  cmphaushmeo  24124  ustexsym  24540  pi1xfrcnv  25383  dvlog  26984  efopnlem2  26990  gtiso  33341  cycpmconjvlem  33748  cycpmconjs  33763  f1ocan2fv  38754  relcnveq3  39352  relcnveq2  39354  brcnvrabga  39367  dfrel5  39371  elrelscnveq3  39652  elrelscnveq2  39654  ltrncnvnid  41277  relintab  44677  relnonrel  44680  cononrel1  44687  cononrel2  44688  clrellem  44715  clcnvlem  44716  relexpaddss  44811  hfstructfun  46119  3f1oss1  48238  3f1oss2  48239  tposideq  50094