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	$$⊢\mathrm{I}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
2		dmi	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}$$
3		df-fn	$$⊢\mathrm{I}Fn\mathrm{V}\leftrightarrow \left(\mathrm{Fun}\mathrm{I}\wedge \mathrm{dom}\mathrm{I}=\mathrm{V}\right)$$
4	1 2 3	mpbir2an	$$⊢\mathrm{I}Fn\mathrm{V}$$