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

Theorem dfrel2 5126
Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
dfrel2  |-  ( Rel 
R  <->  `' `' R  =  R
)

Proof of Theorem dfrel2
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relcnv 5053 . . 3  |-  Rel  `' `' R
2 vex 2793 . . . . . 6  |-  x  e. 
_V
3 vex 2793 . . . . . 6  |-  y  e. 
_V
42, 3opelcnv 4865 . . . . 5  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. y ,  x >.  e.  `' R )
53, 2opelcnv 4865 . . . . 5  |-  ( <.
y ,  x >.  e.  `' R  <->  <. x ,  y
>.  e.  R )
64, 5bitri 240 . . . 4  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. x ,  y
>.  e.  R )
76eqrelriv 4782 . . 3  |-  ( ( Rel  `' `' R  /\  Rel  R )  ->  `' `' R  =  R
)
81, 7mpan 651 . 2  |-  ( Rel 
R  ->  `' `' R  =  R )
9 releq 4773 . . 3  |-  ( `' `' R  =  R  ->  ( Rel  `' `' R 
<->  Rel  R ) )
101, 9mpbii 202 . 2  |-  ( `' `' R  =  R  ->  Rel  R )
118, 10impbii 180 1  |-  ( Rel 
R  <->  `' `' R  =  R
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1625    e. wcel 1686   <.cop 3645   `'ccnv 4690   Rel wrel 4696
This theorem is referenced by:  dfrel4v  5127  cnvcnv  5128  cnveqb  5131  dfrel3  5133  cnvcnvres  5138  cnvsn  5157  cores2  5187  co01  5189  coi2  5191  relcnvtr  5194  relcnvexb  5212  funcnvres2  5325  f1cnvcnv  5447  f1ocnv  5487  f1ocnvb  5488  f1ococnv1  5504  isores1  5833  cnvf1o  6219  fnwelem  6232  tposf12  6261  ssenen  7037  cantnffval2  7399  fsumcnv  12238  structcnvcnv  13161  imasless  13444  oppcinv  13680  cnvps  14323  cnvpsb  14324  cnvtsr  14333  gimcnv  14733  lmimcnv  15822  hmeocnv  17455  hmeocnvb  17467  cmphaushmeo  17493  pi1xfrcnv  18557  dvlog  20000  efopnlem2  20006  fimacnvinrn  23201  gtiso  23243  relexprel  24033  twsymr  25089  dupre2  25255  mxlmnl2  25281  supwval  25295  f1ocan2fv  26406  ltrncnvnid  30389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698  df-cnv 4699
  Copyright terms: Public domain W3C validator