Theorem dfrel2 6136

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ⟨cop 4582  ^◡ccnv 5615  Rel wrel 5621

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622  df-rel 5623  df-cnv 5624

This theorem is referenced by:  dfrel4v  6137  cnvcnv  6139  cnveqb  6143  dfrel3  6145  cnvcnvres  6152  cnvsng  6170  cores2  6207  co01  6209  coi2  6211  relcnvtrg  6214  funcnvres2  6561  f1cnvcnv  6728  f1ocnv  6775  f1ocnvb  6776  f1ococnv1  6792  fimacnvinrn  7004  isores1  7268  relcnvexb  7856  cnvf1o  8041  fnwelem  8061  tposf12  8181  ssenen  9064  f1oenfirn  9089  f1domfi  9090  cantnffval2  9585  fsumcnv  15680  fprodcnv  15890  structcnvcnv  17064  imasless  17444  oppcinv  17687  cnvps  18484  cnvpsb  18485  cnvtsr  18494  gimcnv  19180  rngimcnv  20375  lmimcnv  21002  hmeocnv  23678  hmeocnvb  23690  cmphaushmeo  23716  ustexsym  24132  pi1xfrcnv  24985  dvlog  26588  efopnlem2  26594  gtiso  32680  cycpmconjvlem  33108  cycpmconjs  33123  f1ocan2fv  37773  relcnveq3  38361  relcnveq2  38363  brcnvrabga  38376  dfrel5  38380  elrelscnveq3  38534  elrelscnveq2  38536  ltrncnvnid  40172  rimcnv  42556  relintab  43622  cnvssb  43625  relnonrel  43626  cononrel1  43633  cononrel2  43634  clrellem  43661  clcnvlem  43662  relexpaddss  43757  3f1oss1  47112  3f1oss2  47113  tposideq  48925