Theorem dfrel2 3482

Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.

Assertion

Ref	Expression
dfrel2	|- (Rel R <-> `'`'R = R)

Proof of Theorem dfrel2

Step	Hyp	Ref	Expression
1		relcnv 3432	. . 3 |- Rel `'`'R
2		visset 1811	. . . . . . 7 |- x e. V
3		visset 1811	. . . . . . 7 |- y e. V
4	2, 3	opelcnv 3295	. . . . . 6 |- (<.x, y>. e. `'`'R <-> <.y, x>. e. `'R)
5	3, 2	opelcnv 3295	. . . . . 6 |- (<.y, x>. e. `'R <-> <.x, y>. e. R)
6	4, 5	bitr 173	. . . . 5 |- (<.x, y>. e. `'`'R <-> <.x, y>. e. R)
7	6	gen2 982	. . . 4 |- A.xA.y(<.x, y>. e. `'`'R <-> <.x, y>. e. R)
8		eqrel 3247	. . . 4 |- ((Rel `'`'R /\ Rel R) -> (`'`'R = R <-> A.xA.y(<.x, y>. e. `'`'R <-> <.x, y>. e. R)))
9	7, 8	mpbiri 194	. . 3 |- ((Rel `'`'R /\ Rel R) -> `'`'R = R)
10	1, 9	mpan 694	. 2 |- (Rel R -> `'`'R = R)
11		releq 3240	. . 3 |- (`'`'R = R -> (Rel `'`'R <-> Rel R))
12	1, 11	mpbii 193	. 2 |- (`'`'R = R -> Rel R)
13	10, 12	impbi 157	1 |- (Rel R <-> `'`'R = R)

Syntax hints:   <-> wb 146   /\ wa 223  A.wal 953   = wceq 955   e. wcel 957  <.cop 2409  `'ccnv 3166  Rel wrel 3172

This theorem is referenced by:  cnvcnv 3483  dfrel3 3486  cnvcnvres 3491  cores2 3504  co01 3506  coi2 3508  relcnvexb 3518  funcnvres2 3567  f1cnv 3663  f1ocnvb 3699  f1ococnv1 3706  ssenen 4497  cnvhmpha 10506  cnvhmphb 10507  cnvhmph 10508  hmphsyma 10509

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-pr 2776

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-br 2617  df-opab 2664  df-xp 3181  df-rel 3182  df-cnv 3183

Copyright terms: Public domain