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	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{f|\left(f:A⟶B\wedge f:A⟶B\right)\right\}=\left\{f|\left(f:A⟶B\wedge f:A⟶B\right)\right\}$$
2	1	fabexg	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|\left(f:A⟶B\wedge f:A⟶B\right)\right\}\in \mathrm{V}$$
3		id	$$⊢f:A⟶B\to f:A⟶B$$
4	3	ancli	$$⊢f:A⟶B\to \left(f:A⟶B\wedge f:A⟶B\right)$$
5	4	ss2abi	$$⊢\left\{f|f:A⟶B\right\}\subseteq \left\{f|\left(f:A⟶B\wedge f:A⟶B\right)\right\}$$
6	5	a1i	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|f:A⟶B\right\}\subseteq \left\{f|\left(f:A⟶B\wedge f:A⟶B\right)\right\}$$
7	2 6	ssexd	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$