Theorem dfrel2 5733

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 5653	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3335	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3335	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5451	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5451	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 264	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5362	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 708	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5350	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 223	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 199	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 196   = wceq 1624   ∈ wcel 2131  ⟨cop 4319  ^◡ccnv 5257  Rel wrel 5263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857  df-xp 5264  df-rel 5265  df-cnv 5266

This theorem is referenced by:  dfrel4v  5734  cnvcnv  5736  cnvcnvOLD  5737  cnveqb  5740  dfrel3  5742  cnvcnvres  5748  cnvsng  5767  cnvsnOLD  5771  cores2  5801  co01  5803  coi2  5805  relcnvtr  5808  funcnvres2  6122  f1cnvcnv  6262  f1ocnv  6302  f1ocnvb  6303  f1ococnv1  6318  fimacnvinrn  6503  isores1  6739  relcnvexb  7271  cnvf1o  7436  fnwelem  7452  tposf12  7538  ssenen  8291  cantnffval2  8757  fsumcnv  14695  fprodcnv  14904  structcnvcnv  16065  imasless  16394  oppcinv  16633  cnvps  17405  cnvpsb  17406  cnvtsr  17415  gimcnv  17902  lmimcnv  19261  hmeocnv  21759  hmeocnvb  21771  cmphaushmeo  21797  ustexsym  22212  pi1xfrcnv  23049  dvlog  24588  efopnlem2  24594  gtiso  29779  f1ocan2fv  33827  relcnveq3  34408  relcnveq2  34410  dfrel5  34429  elrelscnveq3  34556  elrelscnveq2  34558  ltrncnvnid  35908  relintab  38383  cnvssb  38386  relnonrel  38387  cononrel1  38394  cononrel2  38395  clrellem  38423  clcnvlem  38424  relexpaddss  38504