Theorem dfrel2 5395

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 5313	. . 3 |- Rel `' `' R
2		vex 3079	. . . . . 6 |- x e. _V
3		vex 3079	. . . . . 6 |- y e. _V
4	2, 3	opelcnv 5128	. . . . 5 |- ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5	3, 2	opelcnv 5128	. . . . 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 5040	. . 3 |- ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8	1, 7	mpan 670	. 2 |- ( Rel R -> `' `' R = R )
9		releq 5029	. . 3 |- ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10	1, 9	mpbii 211	. 2 |- ( `' `' R = R -> Rel R )
11	8, 10	impbii 188	1 |- ( Rel R <-> `' `' R = R )

Syntax hints:   <-> wb 184   = wceq 1370   e. wcel 1758   <.cop 3990   `'ccnv 4946   Rel wrel 4952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-xp 4953  df-rel 4954  df-cnv 4955

This theorem is referenced by:  dfrel4v  5396  cnvcnv  5397  cnveqb  5400  dfrel3  5402  cnvcnvres  5409  cnvsn  5429  cores2  5457  co01  5459  coi2  5461  relcnvtr  5464  funcnvres2  5596  f1cnvcnv  5721  f1ocnv  5760  f1ocnvb  5761  f1ococnv1  5776  isores1  6133  relcnvexb  6635  cnvf1o  6780  fnwelem  6796  tposf12  6879  ssenen  7594  cantnffval2  8013  cantnffval2OLD  8035  fsumcnv  13357  structcnvcnv  14302  imasless  14596  oppcinv  14832  cnvps  15500  cnvpsb  15501  cnvtsr  15510  gimcnv  15913  lmimcnv  17270  hmeocnv  19466  hmeocnvb  19478  cmphaushmeo  19504  ustexsym  19921  pi1xfrcnv  20760  dvlog  22228  efopnlem2  22234  fimacnvinrn  26102  gtiso  26146  relexprel  27479  fprodcnv  27637  f1ocan2fv  28768  ltrncnvnid  34094