Description: The identity relation is a function. Part of Theorem 10.4 of Quine p. 65. See also idfn . (Contributed by NM, 30Apr1998)
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  axmp   ( _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  dffun   ( Fun _I <> ( Rel _I /\ ( _I o. `' _I ) C_ _I ) ) 

9  1 7 8  mpbir2an   Fun _I 