Theorem dfrel2 5038

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 4966	. . 3 |- Rel `' `' R
2		vex 2715	. . . . . 6 |- x e. _V
3		vex 2715	. . . . . 6 |- y e. _V
4	2, 3	opelcnv 4770	. . . . 5 |- ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5	3, 2	opelcnv 4770	. . . . 5 |- ( <. y , x >. e. `' R <-> <. x , y >. e. R )
6	4, 5	bitri 183	. . . 4 |- ( <. x , y >. e. `' `' R <-> <. x , y >. e. R )
7	6	eqrelriv 4681	. . 3 |- ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8	1, 7	mpan 421	. 2 |- ( Rel R -> `' `' R = R )
9		releq 4670	. . 3 |- ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10	1, 9	mpbii 147	. 2 |- ( `' `' R = R -> Rel R )
11	8, 10	impbii 125	1 |- ( Rel R <-> `' `' R = R )

Syntax hints:   <-> wb 104   = wceq 1335   e. wcel 2128   <.cop 3564   `'ccnv 4587   Rel wrel 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4084  ax-pow 4137  ax-pr 4171

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-br 3968  df-opab 4028  df-xp 4594  df-rel 4595  df-cnv 4596

This theorem is referenced by:  dfrel4v  5039  cnvcnv  5040  cnveqb  5043  dfrel3  5045  cnvcnvres  5051  cnvsn  5070  cores2  5100  co01  5102  coi2  5104  relcnvtr  5107  relcnvexb  5127  funcnvres2  5247  f1cnvcnv  5388  f1ocnv  5429  f1ocnvb  5430  f1ococnv1  5445  isores1  5766  cnvf1o  6174  tposf12  6218  ssenen  6798  relcnvfi  6887  caseinl  7037  caseinr  7038  fsumcnv  11345  fprodcnv  11533  structcnvcnv  12276  hmeocnv  12777  hmeocnvb  12788