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

Theorem dfrel2 6039
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 5960 . . 3 Rel 𝑅
2 vex 3495 . . . . . 6 𝑥 ∈ V
3 vex 3495 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5745 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5745 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 276 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5655 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 686 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5644 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 234 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 210 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wcel 2105  cop 4563  ccnv 5547  Rel wrel 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556
This theorem is referenced by:  dfrel4v  6040  cnvcnv  6042  cnveqb  6046  dfrel3  6048  cnvcnvres  6055  cnvsng  6073  cores2  6105  co01  6107  coi2  6109  relcnvtrg  6112  funcnvres2  6427  f1cnvcnv  6577  f1ocnv  6620  f1ocnvb  6621  f1ococnv1  6636  fimacnvinrn  6832  isores1  7076  relcnvexb  7620  cnvf1o  7795  fnwelem  7814  tposf12  7906  ssenen  8679  cantnffval2  9146  fsumcnv  15116  fprodcnv  15325  structcnvcnv  16485  imasless  16801  oppcinv  17038  cnvps  17810  cnvpsb  17811  cnvtsr  17820  gimcnv  18345  lmimcnv  19768  hmeocnv  22298  hmeocnvb  22310  cmphaushmeo  22336  ustexsym  22751  pi1xfrcnv  23588  dvlog  25161  efopnlem2  25167  gtiso  30362  cycpmconjvlem  30710  cycpmconjs  30725  f1ocan2fv  34883  relcnveq3  35459  relcnveq2  35461  brcnvrabga  35480  dfrel5  35484  elrelscnveq3  35611  elrelscnveq2  35613  ltrncnvnid  37143  relintab  39821  cnvssb  39824  relnonrel  39825  cononrel1  39832  cononrel2  39833  clrellem  39860  clcnvlem  39861  relexpaddss  39941
  Copyright terms: Public domain W3C validator