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 )

Metamath Proof Explorer

Theorem mapex

Proof