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

Theorem dfrel2 6092
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 6012 . . 3 Rel 𝑅
2 vex 3436 . . . . . 6 𝑥 ∈ V
3 vex 3436 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5790 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5790 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 274 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5699 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 687 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5687 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 232 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 208 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1539  wcel 2106  cop 4567  ccnv 5588  Rel wrel 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597
This theorem is referenced by:  dfrel4v  6093  cnvcnv  6095  cnveqb  6099  dfrel3  6101  cnvcnvres  6108  cnvsng  6126  cores2  6163  co01  6165  coi2  6167  relcnvtrg  6170  funcnvres2  6514  f1cnvcnv  6680  f1ocnv  6728  f1ocnvb  6729  f1ococnv1  6745  fimacnvinrn  6949  isores1  7205  relcnvexb  7773  cnvf1o  7951  fnwelem  7972  tposf12  8067  ssenen  8938  f1oenfirn  8966  f1domfi  8967  cantnffval2  9453  fsumcnv  15485  fprodcnv  15693  structcnvcnv  16854  imasless  17251  oppcinv  17492  cnvps  18296  cnvpsb  18297  cnvtsr  18306  gimcnv  18883  lmimcnv  20329  hmeocnv  22913  hmeocnvb  22925  cmphaushmeo  22951  ustexsym  23367  pi1xfrcnv  24220  dvlog  25806  efopnlem2  25812  gtiso  31033  cycpmconjvlem  31408  cycpmconjs  31423  f1ocan2fv  35885  relcnveq3  36456  relcnveq2  36458  brcnvrabga  36477  dfrel5  36481  elrelscnveq3  36609  elrelscnveq2  36611  ltrncnvnid  38141  relintab  41191  cnvssb  41194  relnonrel  41195  cononrel1  41202  cononrel2  41203  clrellem  41230  clcnvlem  41231  relexpaddss  41326
  Copyright terms: Public domain W3C validator