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

Theorem dfrel2 5485
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 5406 . . 3 Rel 𝑅
2 vex 3172 . . . . . 6 𝑥 ∈ V
3 vex 3172 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5211 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5211 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 262 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5122 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 701 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5111 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 221 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 197 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976  cop 4127  ccnv 5024  Rel wrel 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-xp 5031  df-rel 5032  df-cnv 5033
This theorem is referenced by:  dfrel4v  5486  cnvcnv  5488  cnveqb  5491  dfrel3  5493  cnvcnvres  5499  cnvsn  5519  cores2  5548  co01  5550  coi2  5552  relcnvtr  5555  funcnvres2  5866  f1cnvcnv  6004  f1ocnv  6044  f1ocnvb  6045  f1ococnv1  6060  fimacnvinrn  6238  isores1  6459  relcnvexb  6981  cnvf1o  7137  fnwelem  7153  tposf12  7238  ssenen  7993  cantnffval2  8449  fsumcnv  14289  fprodcnv  14495  structcnvcnv  15649  imasless  15966  oppcinv  16206  cnvps  16978  cnvpsb  16979  cnvtsr  16988  gimcnv  17475  lmimcnv  18831  hmeocnv  21314  hmeocnvb  21326  cmphaushmeo  21352  ustexsym  21768  pi1xfrcnv  22593  dvlog  24111  efopnlem2  24117  gtiso  28664  f1ocan2fv  32492  ltrncnvnid  34231  relintab  36708  cnvssb  36711  relnonrel  36712  cononrel1  36719  cononrel2  36720  clrellem  36748  clcnvlem  36749  relexpaddss  36829
  Copyright terms: Public domain W3C validator