MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfrel2 Structured version   Visualization version   GIF version

Theorem dfrel2 5552
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.
StepHypRef Expression
1 relcnv 5472 . . 3 Rel 𝑅
2 vex 3193 . . . . . 6 𝑥 ∈ V
3 vex 3193 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5274 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5274 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 264 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5184 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 705 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5172 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 223 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 199 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1480  wcel 1987  cop 4161  ccnv 5083  Rel wrel 5089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-rel 5091  df-cnv 5092
This theorem is referenced by:  dfrel4v  5553  cnvcnv  5555  cnvcnvOLD  5556  cnveqb  5559  dfrel3  5561  cnvcnvres  5567  cnvsn  5587  cores2  5617  co01  5619  coi2  5621  relcnvtr  5624  funcnvres2  5937  f1cnvcnv  6076  f1ocnv  6116  f1ocnvb  6117  f1ococnv1  6132  fimacnvinrn  6314  isores1  6549  relcnvexb  7076  cnvf1o  7236  fnwelem  7252  tposf12  7337  ssenen  8094  cantnffval2  8552  fsumcnv  14451  fprodcnv  14657  structcnvcnv  15813  imasless  16140  oppcinv  16380  cnvps  17152  cnvpsb  17153  cnvtsr  17162  gimcnv  17649  lmimcnv  19007  hmeocnv  21505  hmeocnvb  21517  cmphaushmeo  21543  ustexsym  21959  pi1xfrcnv  22797  dvlog  24331  efopnlem2  24337  gtiso  29362  f1ocan2fv  33193  ltrncnvnid  34932  relintab  37409  cnvssb  37412  relnonrel  37413  cononrel1  37420  cononrel2  37421  clrellem  37449  clcnvlem  37450  relexpaddss  37530
  Copyright terms: Public domain W3C validator