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

Theorem dfrel2 5079
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 5006 . . 3 Rel 𝑅
2 vex 2740 . . . . . 6 𝑥 ∈ V
3 vex 2740 . . . . . 6 𝑦 ∈ V
42, 3opelcnv 4809 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
53, 2opelcnv 4809 . . . . 5 (⟨𝑦, 𝑥⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
64, 5bitri 184 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
76eqrelriv 4719 . . 3 ((Rel 𝑅 ∧ Rel 𝑅) → 𝑅 = 𝑅)
81, 7mpan 424 . 2 (Rel 𝑅𝑅 = 𝑅)
9 releq 4708 . . 3 (𝑅 = 𝑅 → (Rel 𝑅 ↔ Rel 𝑅))
101, 9mpbii 148 . 2 (𝑅 = 𝑅 → Rel 𝑅)
118, 10impbii 126 1 (Rel 𝑅𝑅 = 𝑅)
Colors of variables: wff set class
Syntax hints:  wb 105   = wceq 1353  wcel 2148  cop 3595  ccnv 4625  Rel wrel 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-rel 4633  df-cnv 4634
This theorem is referenced by:  dfrel4v  5080  cnvcnv  5081  cnveqb  5084  dfrel3  5086  cnvcnvres  5092  cnvsn  5111  cores2  5141  co01  5143  coi2  5145  relcnvtr  5148  relcnvexb  5168  funcnvres2  5291  f1cnvcnv  5432  f1ocnv  5474  f1ocnvb  5475  f1ococnv1  5490  isores1  5814  cnvf1o  6225  tposf12  6269  ssenen  6850  relcnvfi  6939  caseinl  7089  caseinr  7090  fsumcnv  11444  fprodcnv  11632  structcnvcnv  12477  hmeocnv  13743  hmeocnvb  13754
  Copyright terms: Public domain W3C validator