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 e. C /\ B e. D ) -> { f | f : A --> B } e. _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 e. C /\ B e. D ) -> { f | ( f : A --> B /\ f : A --> B ) } e. _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 } C_ { f | ( f : A --> B /\ f : A --> B ) }
6	5	a1i	|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } C_ { f | ( f : A --> B /\ f : A --> B ) } )
7	2 6	ssexd	|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )