Metamath Proof Explorer


Theorem mapex

Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003) (Proof shortened by AV, 16-Jun-2025)

Ref Expression
Assertion mapex A C B D f | f : A B V

Proof

Step Hyp Ref Expression
1 eqid f | f : A B f : A B = f | f : A B f : A B
2 1 fabexg A C B D f | f : A B f : A B V
3 id f : A B f : A B
4 3 ancli f : A B f : A B f : A B
5 4 ss2abi f | f : A B f | f : A B f : A B
6 5 a1i A C B D f | f : A B f | f : A B f : A B
7 2 6 ssexd A C B D f | f : A B V