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

Theorem dfrel2 5801
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 5720 . . 3 Rel 𝑅
2 vex 3401 . . . . . 6 𝑥 ∈ V
3 vex 3401 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5512 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5512 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 266 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5422 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 673 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5410 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 224 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 200 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637  wcel 2157  cop 4383  ccnv 5317  Rel wrel 5323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852  df-opab 4914  df-xp 5324  df-rel 5325  df-cnv 5326
This theorem is referenced by:  dfrel4v  5802  cnvcnv  5804  cnvcnvOLD  5805  cnveqb  5808  dfrel3  5810  cnvcnvres  5816  cnvsng  5835  cnvsnOLD  5839  cores2  5869  co01  5871  coi2  5873  relcnvtr  5876  funcnvres2  6183  f1cnvcnv  6328  f1ocnv  6368  f1ocnvb  6369  f1ococnv1  6384  fimacnvinrn  6573  isores1  6811  relcnvexb  7347  cnvf1o  7513  fnwelem  7529  tposf12  7615  ssenen  8376  cantnffval2  8842  fsumcnv  14730  fprodcnv  14937  structcnvcnv  16085  imasless  16408  oppcinv  16647  cnvps  17420  cnvpsb  17421  cnvtsr  17430  gimcnv  17914  lmimcnv  19277  hmeocnv  21783  hmeocnvb  21795  cmphaushmeo  21821  ustexsym  22236  pi1xfrcnv  23073  dvlog  24617  efopnlem2  24623  gtiso  29811  f1ocan2fv  33836  relcnveq3  34409  relcnveq2  34411  dfrel5  34429  elrelscnveq3  34556  elrelscnveq2  34558  ltrncnvnid  35909  relintab  38390  cnvssb  38393  relnonrel  38394  cononrel1  38401  cononrel2  38402  clrellem  38430  clcnvlem  38431  relexpaddss  38511
  Copyright terms: Public domain W3C validator