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

Theorem dfrel2 5261
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 5182 . . 3  |-  Rel  `' `' R
2 vex 2902 . . . . . 6  |-  x  e. 
_V
3 vex 2902 . . . . . 6  |-  y  e. 
_V
42, 3opelcnv 4994 . . . . 5  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. y ,  x >.  e.  `' R )
53, 2opelcnv 4994 . . . . 5  |-  ( <.
y ,  x >.  e.  `' R  <->  <. x ,  y
>.  e.  R )
64, 5bitri 241 . . . 4  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. x ,  y
>.  e.  R )
76eqrelriv 4909 . . 3  |-  ( ( Rel  `' `' R  /\  Rel  R )  ->  `' `' R  =  R
)
81, 7mpan 652 . 2  |-  ( Rel 
R  ->  `' `' R  =  R )
9 releq 4899 . . 3  |-  ( `' `' R  =  R  ->  ( Rel  `' `' R 
<->  Rel  R ) )
101, 9mpbii 203 . 2  |-  ( `' `' R  =  R  ->  Rel  R )
118, 10impbii 181 1  |-  ( Rel 
R  <->  `' `' R  =  R
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1717   <.cop 3760   `'ccnv 4817   Rel wrel 4823
This theorem is referenced by:  dfrel4v  5262  cnvcnv  5263  cnveqb  5266  dfrel3  5268  cnvcnvres  5273  cnvsn  5292  cores2  5322  co01  5324  coi2  5326  relcnvtr  5329  relcnvexb  5347  funcnvres2  5464  f1cnvcnv  5587  f1ocnv  5627  f1ocnvb  5628  f1ococnv1  5644  isores1  5993  cnvf1o  6384  fnwelem  6397  tposf12  6440  ssenen  7217  cantnffval2  7584  fsumcnv  12484  structcnvcnv  13407  imasless  13692  oppcinv  13928  cnvps  14571  cnvpsb  14572  cnvtsr  14581  gimcnv  14981  lmimcnv  16066  hmeocnv  17715  hmeocnvb  17727  cmphaushmeo  17753  ustexsym  18166  pi1xfrcnv  18953  dvlog  20409  efopnlem2  20415  fimacnvinrn  23890  gtiso  23929  relexprel  24913  f1ocan2fv  26120  ltrncnvnid  30241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-cnv 4826
  Copyright terms: Public domain W3C validator