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