Theorem dfrel2 6180

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 6098	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3455	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3455	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5859	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5859	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 278	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5765	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 703	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5753	. . 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 2145  ⟨cop 4590  ^◡ccnv 5650  Rel wrel 5656

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659

This theorem is used by:  dfrel4v  6181  cnvcnv  6183  cnveqb  6188  dfrel3  6190  cnvcnvres  6199  cnvsng  6217  cores2  6254  co01  6256  coi2  6258  relcnvtrgOLD  6262  funcnvres2  6612  f1cnvcnv  6781  f1ocnv  6829  f1ocnvb  6830  f1ococnv1  6846  fimacnvinrn  7063  isores1  7334  relcnvexb  7927  cnvf1o  8111  fnwelem  8132  tposf12  8252  ssenen  9154  f1oenfirn  9179  f1domfi  9180  cantnffval2  9680  fsumcnv  15919  fprodcnv  16130  structcnvcnv  17311  imasless  17692  oppcinv  17935  cnvps  18732  cnvpsb  18733  cnvtsr  18742  gimcnv  19461  rngimcnv  20666  rimcnv  20697  lmimcnv  21322  hmeocnv  24061  hmeocnvb  24073  cmphaushmeo  24099  ustexsym  24515  pi1xfrcnv  25358  dvlog  26961  efopnlem2  26967  gtiso  33276  cycpmconjvlem  33684  cycpmconjs  33699  f1ocan2fv  38629  relcnveq3  39227  relcnveq2  39229  brcnvrabga  39242  dfrel5  39246  elrelscnveq3  39527  elrelscnveq2  39529  ltrncnvnid  41152  relintab  44542  cnvssb  44545  relnonrel  44546  cononrel1  44553  cononrel2  44554  clrellem  44581  clcnvlem  44582  relexpaddss  44677  3f1oss1  48089  3f1oss2  48090  tposideq  49940