Theorem dfrel2 6177

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 6092	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3477	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3477	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5873	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5873	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 274	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5781	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 688	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5768	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 232	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 208	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ⟨cop 4628  ^◡ccnv 5668  Rel wrel 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-xp 5675  df-rel 5676  df-cnv 5677

This theorem is referenced by:  dfrel4v  6178  cnvcnv  6180  cnveqb  6184  dfrel3  6186  cnvcnvres  6193  cnvsng  6211  cores2  6247  co01  6249  coi2  6251  relcnvtrg  6254  funcnvres2  6617  f1cnvcnv  6784  f1ocnv  6832  f1ocnvb  6833  f1ococnv1  6849  fimacnvinrn  7058  isores1  7315  relcnvexb  7899  cnvf1o  8079  fnwelem  8099  tposf12  8218  ssenen  9134  f1oenfirn  9166  f1domfi  9167  cantnffval2  9672  fsumcnv  15701  fprodcnv  15909  structcnvcnv  17068  imasless  17468  oppcinv  17709  cnvps  18513  cnvpsb  18514  cnvtsr  18523  gimcnv  19107  lmimcnv  20627  hmeocnv  23195  hmeocnvb  23207  cmphaushmeo  23233  ustexsym  23649  pi1xfrcnv  24502  dvlog  26088  efopnlem2  26094  gtiso  31793  cycpmconjvlem  32171  cycpmconjs  32186  f1ocan2fv  36400  relcnveq3  36995  relcnveq2  36997  brcnvrabga  37016  dfrel5  37020  elrelscnveq3  37166  elrelscnveq2  37168  ltrncnvnid  38803  rimcnv  40896  relintab  42105  cnvssb  42108  relnonrel  42109  cononrel1  42116  cononrel2  42117  clrellem  42144  clcnvlem  42145  relexpaddss  42240