This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idfn

Description: The identity relation is a function on the universal class. See also funi . (Contributed by BJ, 23-Dec-2023)

Ref Expression
Assertion idfn 
|- _I Fn _V

Proof

Step Hyp Ref Expression
1 funi 
 |-  Fun _I
2 dmi 
 |-  dom _I = _V
3 df-fn 
 |-  ( _I Fn _V <-> ( Fun _I /\ dom _I = _V ) )
4 1 2 3 mpbir2an 
 |-  _I Fn _V