ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfrel2 GIF version

Theorem dfrel2 4959
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 4887 . . 3 Rel 𝑅
2 vex 2663 . . . . . 6 𝑥 ∈ V
3 vex 2663 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 4691 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 4691 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 183 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 4602 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 420 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 4591 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 147 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 125 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1316  wcel 1465  cop 3500  ccnv 4508  Rel wrel 4514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900  df-opab 3960  df-xp 4515  df-rel 4516  df-cnv 4517
This theorem is referenced by:  dfrel4v  4960  cnvcnv  4961  cnveqb  4964  dfrel3  4966  cnvcnvres  4972  cnvsn  4991  cores2  5021  co01  5023  coi2  5025  relcnvtr  5028  relcnvexb  5048  funcnvres2  5168  f1cnvcnv  5309  f1ocnv  5348  f1ocnvb  5349  f1ococnv1  5364  isores1  5683  cnvf1o  6090  tposf12  6134  ssenen  6713  relcnvfi  6797  caseinl  6944  caseinr  6945  fsumcnv  11174  structcnvcnv  11902  hmeocnv  12403  hmeocnvb  12414
  Copyright terms: Public domain W3C validator