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

Theorem dfrel2 6177
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 6092 . . 3 Rel 𝑅
2 vex 3477 . . . . . 6 𝑥 ∈ V
3 vex 3477 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5873 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5873 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 274 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5781 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 688 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5768 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 232 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 208 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  cop 4628  ccnv 5668  Rel wrel 5674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-xp 5675  df-rel 5676  df-cnv 5677
This theorem is referenced by:  dfrel4v  6178  cnvcnv  6180  cnveqb  6184  dfrel3  6186  cnvcnvres  6193  cnvsng  6211  cores2  6247  co01  6249  coi2  6251  relcnvtrg  6254  funcnvres2  6617  f1cnvcnv  6784  f1ocnv  6832  f1ocnvb  6833  f1ococnv1  6849  fimacnvinrn  7058  isores1  7315  relcnvexb  7899  cnvf1o  8079  fnwelem  8099  tposf12  8218  ssenen  9134  f1oenfirn  9166  f1domfi  9167  cantnffval2  9672  fsumcnv  15701  fprodcnv  15909  structcnvcnv  17068  imasless  17468  oppcinv  17709  cnvps  18513  cnvpsb  18514  cnvtsr  18523  gimcnv  19107  lmimcnv  20627  hmeocnv  23195  hmeocnvb  23207  cmphaushmeo  23233  ustexsym  23649  pi1xfrcnv  24502  dvlog  26088  efopnlem2  26094  gtiso  31793  cycpmconjvlem  32171  cycpmconjs  32186  f1ocan2fv  36400  relcnveq3  36995  relcnveq2  36997  brcnvrabga  37016  dfrel5  37020  elrelscnveq3  37166  elrelscnveq2  37168  ltrncnvnid  38803  rimcnv  40896  relintab  42105  cnvssb  42108  relnonrel  42109  cononrel1  42116  cononrel2  42117  clrellem  42144  clcnvlem  42145  relexpaddss  42240
  Copyright terms: Public domain W3C validator