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

Theorem dfrel2 6027
 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 5948 . . 3 Rel 𝑅
2 vex 3482 . . . . . 6 𝑥 ∈ V
3 vex 3482 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 5733 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 5733 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 278 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 5643 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 689 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 5632 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 236 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 212 1 (Rel 𝑅𝑅 = 𝑅)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2115  ⟨cop 4554  ◡ccnv 5535  Rel wrel 5541 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pr 5311 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5048  df-opab 5110  df-xp 5542  df-rel 5543  df-cnv 5544 This theorem is referenced by:  dfrel4v  6028  cnvcnv  6030  cnveqb  6034  dfrel3  6036  cnvcnvres  6043  cnvsng  6061  cores2  6093  co01  6095  coi2  6097  relcnvtrg  6100  funcnvres2  6415  f1cnvcnv  6565  f1ocnv  6608  f1ocnvb  6609  f1ococnv1  6624  fimacnvinrn  6821  isores1  7069  relcnvexb  7614  cnvf1o  7789  fnwelem  7808  tposf12  7900  ssenen  8675  cantnffval2  9142  fsumcnv  15117  fprodcnv  15326  structcnvcnv  16486  imasless  16802  oppcinv  17039  cnvps  17811  cnvpsb  17812  cnvtsr  17821  gimcnv  18396  lmimcnv  19825  hmeocnv  22356  hmeocnvb  22368  cmphaushmeo  22394  ustexsym  22810  pi1xfrcnv  23651  dvlog  25231  efopnlem2  25237  gtiso  30433  cycpmconjvlem  30801  cycpmconjs  30816  f1ocan2fv  35065  relcnveq3  35638  relcnveq2  35640  brcnvrabga  35659  dfrel5  35663  elrelscnveq3  35791  elrelscnveq2  35793  ltrncnvnid  37323  relintab  40115  cnvssb  40118  relnonrel  40119  cononrel1  40126  cononrel2  40127  clrellem  40154  clcnvlem  40155  relexpaddss  40251
 Copyright terms: Public domain W3C validator