Description: Alternate definition of relation. Exercise 2 of TakeutiZaring p. 25. (Contributed by NM, 29-Dec-1996) (Proof shortened by BJ, 16-Oct-2026) Do not use opabid2 . (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-dfrel2 | |- ( Rel R <-> `' `' R = R ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-dfrel4v | |- ( Rel R <-> { <. x , y >. | x R y } = R ) |
|
| 2 | cnvcnv3 | |- `' `' R = { <. x , y >. | x R y } |
|
| 3 | 2 | eqeq1i | |- ( `' `' R = R <-> { <. x , y >. | x R y } = R ) |
| 4 | 1 3 | bitr4i | |- ( Rel R <-> `' `' R = R ) |