Theorem dfrel2 6194

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 6113	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5867	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5867	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5771	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 703	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5759	. . 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 2147  ⟨cop 4838  ^◡ccnv 5655  Rel wrel 5661

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664

This theorem is used by:  dfrel4v  6195  cnvcnv  6197  cnvssb  6202  dfrel3  6206  cnvcnvres  6220  cnvsng  6238  cores2  6275  co01  6279  coi2  6281  relcnvtrgOLD  6288  funcnvres2  6645  f1cnvcnv  6814  f1ocnv  6862  f1ocnvb  6863  f1ococnv1  6880  fimacnvinrn  7098  isores1  7368  relcnvexb  7965  cnvf1o  8152  fnwelem  8173  tposf12  8299  ssenen  9201  f1oenfirn  9226  f1domfi  9227  cantnffval2  9726  fsumcnv  15971  fprodcnv  16182  structcnvcnv  17363  imasless  17744  oppcinv  17987  cnvps  18784  cnvpsb  18785  cnvtsr  18794  gimcnv  19513  rngimcnv  20719  rimcnv  20750  lmimcnv  21375  hmeocnv  24114  hmeocnvb  24126  cmphaushmeo  24152  ustexsym  24568  pi1xfrcnv  25411  dvlog  27012  efopnlem2  27018  gtiso  33368  cycpmconjvlem  33778  cycpmconjs  33793  f1ocan2fv  38866  relcnveq3  39462  relcnveq2  39464  brcnvrabga  39477  dfrel5  39481  elrelscnveq3  39762  elrelscnveq2  39764  ltrncnvnid  41387  relintab  44787  relnonrel  44790  cononrel1  44797  cononrel2  44798  clrellem  44825  clcnvlem  44826  relexpaddss  44921  hfstructfun  46235  3f1oss1  48360  3f1oss2  48361  tposideq  50216