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

Theorem dfrel2 5284
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 5205 . . 3  |-  Rel  `' `' R
2 vex 2923 . . . . . 6  |-  x  e. 
_V
3 vex 2923 . . . . . 6  |-  y  e. 
_V
42, 3opelcnv 5017 . . . . 5  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. y ,  x >.  e.  `' R )
53, 2opelcnv 5017 . . . . 5  |-  ( <.
y ,  x >.  e.  `' R  <->  <. x ,  y
>.  e.  R )
64, 5bitri 241 . . . 4  |-  ( <.
x ,  y >.  e.  `' `' R  <->  <. x ,  y
>.  e.  R )
76eqrelriv 4932 . . 3  |-  ( ( Rel  `' `' R  /\  Rel  R )  ->  `' `' R  =  R
)
81, 7mpan 652 . 2  |-  ( Rel 
R  ->  `' `' R  =  R )
9 releq 4922 . . 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 1721   <.cop 3781   `'ccnv 4840   Rel wrel 4846
This theorem is referenced by:  dfrel4v  5285  cnvcnv  5286  cnveqb  5289  dfrel3  5291  cnvcnvres  5296  cnvsn  5315  cores2  5345  co01  5347  coi2  5349  relcnvtr  5352  relcnvexb  5370  funcnvres2  5487  f1cnvcnv  5610  f1ocnv  5650  f1ocnvb  5651  f1ococnv1  5667  isores1  6017  cnvf1o  6408  fnwelem  6424  tposf12  6467  ssenen  7244  cantnffval2  7611  fsumcnv  12516  structcnvcnv  13439  imasless  13724  oppcinv  13960  cnvps  14603  cnvpsb  14604  cnvtsr  14613  gimcnv  15013  lmimcnv  16098  hmeocnv  17751  hmeocnvb  17763  cmphaushmeo  17789  ustexsym  18202  pi1xfrcnv  19039  dvlog  20499  efopnlem2  20505  fimacnvinrn  24004  gtiso  24045  relexprel  25091  fprodcnv  25264  f1ocan2fv  26323  ltrncnvnid  30613
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 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
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 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-xp 4847  df-rel 4848  df-cnv 4849
  Copyright terms: Public domain W3C validator