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