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