Theorem dfrel2 6041

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 5962	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3498	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3498	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5747	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5747	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 277	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5657	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 688	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5646	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 235	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 211	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 208   = wceq 1533   ∈ wcel 2110  ⟨cop 4567  ^◡ccnv 5549  Rel wrel 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060  df-opab 5122  df-xp 5556  df-rel 5557  df-cnv 5558

This theorem is referenced by:  dfrel4v  6042  cnvcnv  6044  cnveqb  6048  dfrel3  6050  cnvcnvres  6057  cnvsng  6075  cores2  6107  co01  6109  coi2  6111  relcnvtrg  6114  funcnvres2  6429  f1cnvcnv  6579  f1ocnv  6622  f1ocnvb  6623  f1ococnv1  6638  fimacnvinrn  6835  isores1  7081  relcnvexb  7625  cnvf1o  7800  fnwelem  7819  tposf12  7911  ssenen  8685  cantnffval2  9152  fsumcnv  15122  fprodcnv  15331  structcnvcnv  16491  imasless  16807  oppcinv  17044  cnvps  17816  cnvpsb  17817  cnvtsr  17826  gimcnv  18401  lmimcnv  19833  hmeocnv  22364  hmeocnvb  22376  cmphaushmeo  22402  ustexsym  22818  pi1xfrcnv  23655  dvlog  25228  efopnlem2  25234  gtiso  30430  cycpmconjvlem  30778  cycpmconjs  30793  f1ocan2fv  34996  relcnveq3  35572  relcnveq2  35574  brcnvrabga  35593  dfrel5  35597  elrelscnveq3  35725  elrelscnveq2  35727  ltrncnvnid  37257  relintab  39936  cnvssb  39939  relnonrel  39940  cononrel1  39947  cononrel2  39948  clrellem  39975  clcnvlem  39976  relexpaddss  40056