Theorem dfrel2 5274

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 5195	. . 3 |- Rel `' `' R
2		vex 3062	. . . . . 6 |- x e. _V
3		vex 3062	. . . . . 6 |- y e. _V
4	2, 3	opelcnv 5005	. . . . 5 |- ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5	3, 2	opelcnv 5005	. . . . 5 |- ( <. y , x >. e. `' R <-> <. x , y >. e. R )
6	4, 5	bitri 249	. . . 4 |- ( <. x , y >. e. `' `' R <-> <. x , y >. e. R )
7	6	eqrelriv 4917	. . 3 |- ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8	1, 7	mpan 668	. 2 |- ( Rel R -> `' `' R = R )
9		releq 4906	. . 3 |- ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10	1, 9	mpbii 211	. 2 |- ( `' `' R = R -> Rel R )
11	8, 10	impbii 187	1 |- ( Rel R <-> `' `' R = R )

Syntax hints:   <-> wb 184   = wceq 1405   e. wcel 1842   <.cop 3978   `'ccnv 4822   Rel wrel 4828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-opab 4454  df-xp 4829  df-rel 4830  df-cnv 4831

This theorem is referenced by:  dfrel4v  5275  cnvcnv  5276  cnveqb  5279  dfrel3  5281  cnvcnvres  5287  cnvsn  5307  cores2  5336  co01  5338  coi2  5340  relcnvtr  5343  funcnvres2  5640  f1cnvcnv  5772  f1ocnv  5811  f1ocnvb  5812  f1ococnv1  5827  isores1  6213  relcnvexb  6732  cnvf1o  6883  fnwelem  6899  tposf12  6983  ssenen  7729  cantnffval2  8146  cantnffval2OLD  8168  fsumcnv  13739  fprodcnv  13939  structcnvcnv  14852  imasless  15154  oppcinv  15393  cnvps  16166  cnvpsb  16167  cnvtsr  16176  gimcnv  16639  lmimcnv  18033  hmeocnv  20555  hmeocnvb  20567  cmphaushmeo  20593  ustexsym  21010  pi1xfrcnv  21849  dvlog  23326  efopnlem2  23332  fimacnvinrn  27918  gtiso  27963  f1ocan2fv  31500  ltrncnvnid  33144  relexpaddss  35697