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

Theorem dfrel2 6021
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 5941 . . 3 Rel 𝑅
2 vex 3402 . . . . . 6 𝑥 ∈ V
3 vex 3402 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5724 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5724 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 278 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5633 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 690 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5622 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 236 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 212 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1542  wcel 2114  cop 4522  ccnv 5524  Rel wrel 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-xp 5531  df-rel 5532  df-cnv 5533
This theorem is referenced by:  dfrel4v  6022  cnvcnv  6024  cnveqb  6028  dfrel3  6030  cnvcnvres  6037  cnvsng  6055  cores2  6092  co01  6094  coi2  6096  relcnvtrg  6099  funcnvres2  6419  f1cnvcnv  6584  f1ocnv  6630  f1ocnvb  6631  f1ococnv1  6646  fimacnvinrn  6849  isores1  7100  relcnvexb  7657  cnvf1o  7832  fnwelem  7851  tposf12  7946  ssenen  8741  f1oenfirn  8780  cantnffval2  9231  fsumcnv  15221  fprodcnv  15429  structcnvcnv  16600  imasless  16916  oppcinv  17155  cnvps  17938  cnvpsb  17939  cnvtsr  17948  gimcnv  18525  lmimcnv  19958  hmeocnv  22513  hmeocnvb  22525  cmphaushmeo  22551  ustexsym  22967  pi1xfrcnv  23809  dvlog  25394  efopnlem2  25400  gtiso  30608  cycpmconjvlem  30985  cycpmconjs  31000  f1ocan2fv  35528  relcnveq3  36099  relcnveq2  36101  brcnvrabga  36120  dfrel5  36124  elrelscnveq3  36252  elrelscnveq2  36254  ltrncnvnid  37784  relintab  40756  cnvssb  40759  relnonrel  40760  cononrel1  40767  cononrel2  40768  clrellem  40795  clcnvlem  40796  relexpaddss  40892
  Copyright terms: Public domain W3C validator