Theorem dfrel2 6192

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 6111	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3462	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3462	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5872	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5872	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5780	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 703	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5768	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 236	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 212	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ⟨cop 4600  ^◡ccnv 5665  Rel wrel 5671

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674

This theorem is used by:  dfrel4v  6193  cnvcnv  6195  cnveqb  6200  dfrel3  6202  cnvcnvres  6211  cnvsng  6229  cores2  6266  co01  6268  coi2  6270  relcnvtrgOLD  6274  funcnvres2  6623  f1cnvcnv  6792  f1ocnv  6840  f1ocnvb  6841  f1ococnv1  6857  fimacnvinrn  7073  isores1  7343  relcnvexb  7932  cnvf1o  8115  fnwelem  8136  tposf12  8256  ssenen  9149  f1oenfirn  9174  f1domfi  9175  cantnffval2  9674  fsumcnv  15850  fprodcnv  16063  structcnvcnv  17238  imasless  17619  oppcinv  17862  cnvps  18659  cnvpsb  18660  cnvtsr  18669  gimcnv  19368  rngimcnv  20571  rimcnv  20602  lmimcnv  21225  hmeocnv  23956  hmeocnvb  23968  cmphaushmeo  23994  ustexsym  24410  pi1xfrcnv  25253  dvlog  26853  efopnlem2  26859  gtiso  33083  cycpmconjvlem  33492  cycpmconjs  33507  f1ocan2fv  38419  relcnveq3  39017  relcnveq2  39019  brcnvrabga  39032  dfrel5  39036  elrelscnveq3  39317  elrelscnveq2  39319  ltrncnvnid  40942  relintab  44350  cnvssb  44353  relnonrel  44354  cononrel1  44361  cononrel2  44362  clrellem  44389  clcnvlem  44390  relexpaddss  44485  3f1oss1  47853  3f1oss2  47854  tposideq  49707