Metamath Proof Explorer


Theorem iprc

Description: The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn . (Contributed by NM, 1-Jan-2007)

Ref Expression
Assertion iprc ¬ I ∈ V

Proof

Step Hyp Ref Expression
1 dmi dom I = V
2 vprc ¬ V ∈ V
3 1 2 eqneltri ¬ dom I ∈ V
4 dmexg ( I ∈ V → dom I ∈ V )
5 3 4 mto ¬ I ∈ V