Theorem dfrel2 6186

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 6104	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3457	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3457	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5865	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5865	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5773	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 703	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5761	. . 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 1570   ∈ wcel 2145  ⟨cop 4593  ^◡ccnv 5658  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667

This theorem is used by:  dfrel4v  6187  cnvcnv  6189  cnveqb  6194  dfrel3  6196  cnvcnvres  6205  cnvsng  6223  cores2  6260  co01  6262  coi2  6264  relcnvtrgOLD  6268  funcnvres2  6617  f1cnvcnv  6786  f1ocnv  6834  f1ocnvb  6835  f1ococnv1  6851  fimacnvinrn  7068  isores1  7339  relcnvexb  7927  cnvf1o  8112  fnwelem  8133  tposf12  8253  ssenen  9153  f1oenfirn  9178  f1domfi  9179  cantnffval2  9678  fsumcnv  15863  fprodcnv  16076  structcnvcnv  17251  imasless  17632  oppcinv  17875  cnvps  18672  cnvpsb  18673  cnvtsr  18682  gimcnv  19400  rngimcnv  20603  rimcnv  20634  lmimcnv  21257  hmeocnv  23994  hmeocnvb  24006  cmphaushmeo  24032  ustexsym  24448  pi1xfrcnv  25291  dvlog  26896  efopnlem2  26902  gtiso  33181  cycpmconjvlem  33589  cycpmconjs  33604  f1ocan2fv  38485  relcnveq3  39083  relcnveq2  39085  brcnvrabga  39098  dfrel5  39102  elrelscnveq3  39383  elrelscnveq2  39385  ltrncnvnid  41008  relintab  44431  cnvssb  44434  relnonrel  44435  cononrel1  44442  cononrel2  44443  clrellem  44470  clcnvlem  44471  relexpaddss  44566  3f1oss1  47971  3f1oss2  47972  tposideq  49822