Theorem dfrel2 5183

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 5110	. . 3 |- Rel `' `' R
2		vex 2803	. . . . . 6 |- x e. _V
3		vex 2803	. . . . . 6 |- y e. _V
4	2, 3	opelcnv 4908	. . . . 5 |- ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5	3, 2	opelcnv 4908	. . . . 5 |- ( <. y , x >. e. `' R <-> <. x , y >. e. R )
6	4, 5	bitri 184	. . . 4 |- ( <. x , y >. e. `' `' R <-> <. x , y >. e. R )
7	6	eqrelriv 4815	. . 3 |- ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8	1, 7	mpan 424	. 2 |- ( Rel R -> `' `' R = R )
9		releq 4804	. . 3 |- ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10	1, 9	mpbii 148	. 2 |- ( `' `' R = R -> Rel R )
11	8, 10	impbii 126	1 |- ( Rel R <-> `' `' R = R )

Syntax hints:   <-> wb 105   = wceq 1395   e. wcel 2200   <.cop 3670   `'ccnv 4720   Rel wrel 4726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-br 4085  df-opab 4147  df-xp 4727  df-rel 4728  df-cnv 4729

This theorem is referenced by:  dfrel4v  5184  cnvcnv  5185  cnveqb  5188  dfrel3  5190  cnvcnvres  5196  cnvsn  5215  cores2  5245  co01  5247  coi2  5249  relcnvtr  5252  relcnvexb  5272  funcnvres2  5400  f1cnvcnv  5548  f1ocnv  5591  f1ocnvb  5592  f1ococnv1  5607  isores1  5948  cnvf1o  6383  tposf12  6428  ssenen  7030  relcnvfi  7129  caseinl  7279  caseinr  7280  fsumcnv  11985  fprodcnv  12173  structcnvcnv  13085  hmeocnv  15018  hmeocnvb  15029