Theorem pmex

Description: The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007)

	Ref	Expression
Assertion	pmex	|- ( ( A e. C /\ B e. D ) -> { f | ( Fun f /\ f C_ ( A X. B ) ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( Fun f /\ f C_ ( A X. B ) ) <-> ( f C_ ( A X. B ) /\ Fun f ) )
2	1	abbii	|- { f | ( Fun f /\ f C_ ( A X. B ) ) } = { f | ( f C_ ( A X. B ) /\ Fun f ) }
3		xpexg	|- ( ( A e. C /\ B e. D ) -> ( A X. B ) e. _V )
4		abssexg	|- ( ( A X. B ) e. _V -> { f | ( f C_ ( A X. B ) /\ Fun f ) } e. _V )
5	3 4	syl	|- ( ( A e. C /\ B e. D ) -> { f | ( f C_ ( A X. B ) /\ Fun f ) } e. _V )
6	2 5	eqeltrid	|- ( ( A e. C /\ B e. D ) -> { f | ( Fun f /\ f C_ ( A X. B ) ) } e. _V )