Description: The identity relation is a function. Part of Theorem 10.4 of Quine p. 65. See also idfn . (Contributed by NM, 30-Apr-1998)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funi | |- Fun _I |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reli | |- Rel _I |
|
| 2 | relcnv | |- Rel `' _I |
|
| 3 | coi2 | |- ( Rel `' _I -> ( _I o. `' _I ) = `' _I ) |
|
| 4 | 2 3 | ax-mp | |- ( _I o. `' _I ) = `' _I |
| 5 | cnvi | |- `' _I = _I |
|
| 6 | 4 5 | eqtri | |- ( _I o. `' _I ) = _I |
| 7 | 6 | eqimssi | |- ( _I o. `' _I ) C_ _I |
| 8 | df-fun | |- ( Fun _I <-> ( Rel _I /\ ( _I o. `' _I ) C_ _I ) ) |
|
| 9 | 1 7 8 | mpbir2an | |- Fun _I |