Theorem dfrel2 6162

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 6075	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3451	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3451	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5845	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5845	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5752	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 690	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5739	. . 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 4595  ^◡ccnv 5637  Rel wrel 5643

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646

This theorem is referenced by:  dfrel4v  6163  cnvcnv  6165  cnveqb  6169  dfrel3  6171  cnvcnvres  6178  cnvsng  6196  cores2  6232  co01  6234  coi2  6236  relcnvtrg  6239  funcnvres2  6596  f1cnvcnv  6765  f1ocnv  6812  f1ocnvb  6813  f1ococnv1  6829  fimacnvinrn  7043  isores1  7309  relcnvexb  7902  cnvf1o  8090  fnwelem  8110  tposf12  8230  ssenen  9115  f1oenfirn  9144  f1domfi  9145  cantnffval2  9648  fsumcnv  15739  fprodcnv  15949  structcnvcnv  17123  imasless  17503  oppcinv  17742  cnvps  18537  cnvpsb  18538  cnvtsr  18547  gimcnv  19199  rngimcnv  20365  lmimcnv  20974  hmeocnv  23649  hmeocnvb  23661  cmphaushmeo  23687  ustexsym  24103  pi1xfrcnv  24957  dvlog  26560  efopnlem2  26566  gtiso  32624  cycpmconjvlem  33098  cycpmconjs  33113  f1ocan2fv  37721  relcnveq3  38309  relcnveq2  38311  brcnvrabga  38324  dfrel5  38328  elrelscnveq3  38482  elrelscnveq2  38484  ltrncnvnid  40121  rimcnv  42505  relintab  43572  cnvssb  43575  relnonrel  43576  cononrel1  43583  cononrel2  43584  clrellem  43611  clcnvlem  43612  relexpaddss  43707  3f1oss1  47076  3f1oss2  47077  tposideq  48876