Theorem dfrel2 5280

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.

Step	Hyp	Ref	Expression
1		relcnv 5201	. . 3 |- Rel `' `' R
2		vex 2919	. . . . . 6 |- x e. _V
3		vex 2919	. . . . . 6 |- y e. _V
4	2, 3	opelcnv 5013	. . . . 5 |- ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5	3, 2	opelcnv 5013	. . . . 5 |- ( <. y , x >. e. `' R <-> <. x , y >. e. R )
6	4, 5	bitri 241	. . . 4 |- ( <. x , y >. e. `' `' R <-> <. x , y >. e. R )
7	6	eqrelriv 4928	. . 3 |- ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8	1, 7	mpan 652	. 2 |- ( Rel R -> `' `' R = R )
9		releq 4918	. . 3 |- ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10	1, 9	mpbii 203	. 2 |- ( `' `' R = R -> Rel R )
11	8, 10	impbii 181	1 |- ( Rel R <-> `' `' R = R )

Syntax hints:   <-> wb 177   = wceq 1649   e. wcel 1721   <.cop 3777   `'ccnv 4836   Rel wrel 4842

This theorem is referenced by:  dfrel4v  5281  cnvcnv  5282  cnveqb  5285  dfrel3  5287  cnvcnvres  5292  cnvsn  5311  cores2  5341  co01  5343  coi2  5345  relcnvtr  5348  relcnvexb  5366  funcnvres2  5483  f1cnvcnv  5606  f1ocnv  5646  f1ocnvb  5647  f1ococnv1  5663  isores1  6013  cnvf1o  6404  fnwelem  6420  tposf12  6463  ssenen  7240  cantnffval2  7607  fsumcnv  12512  structcnvcnv  13435  imasless  13720  oppcinv  13956  cnvps  14599  cnvpsb  14600  cnvtsr  14609  gimcnv  15009  lmimcnv  16094  hmeocnv  17747  hmeocnvb  17759  cmphaushmeo  17785  ustexsym  18198  pi1xfrcnv  19035  dvlog  20495  efopnlem2  20501  fimacnvinrn  24000  gtiso  24041  relexprel  25087  fprodcnv  25260  f1ocan2fv  26319  ltrncnvnid  30609

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 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-rel 4844  df-cnv 4845