Theorem fabexg

Description: Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008)

	Ref	Expression
Hypothesis	fabexg.1	|- F = { x | ( x : A --> B /\ ph ) }
Assertion	fabexg	|- ( ( A e. C /\ B e. D ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		fabexg.1	|- F = { x | ( x : A --> B /\ ph ) }
2		xpexg	|- ( ( A e. C /\ B e. D ) -> ( A X. B ) e. _V )
3		pwexg	|- ( ( A X. B ) e. _V -> ~P ( A X. B ) e. _V )
4		fssxp	|- ( x : A --> B -> x C_ ( A X. B ) )
5		velpw	|- ( x e. ~P ( A X. B ) <-> x C_ ( A X. B ) )
6	4 5	sylibr	|- ( x : A --> B -> x e. ~P ( A X. B ) )
7	6	anim1i	|- ( ( x : A --> B /\ ph ) -> ( x e. ~P ( A X. B ) /\ ph ) )
8	7	ss2abi	|- { x | ( x : A --> B /\ ph ) } C_ { x | ( x e. ~P ( A X. B ) /\ ph ) }
9	1 8	eqsstri	|- F C_ { x | ( x e. ~P ( A X. B ) /\ ph ) }
10		ssab2	|- { x | ( x e. ~P ( A X. B ) /\ ph ) } C_ ~P ( A X. B )
11	9 10	sstri	|- F C_ ~P ( A X. B )
12		ssexg	|- ( ( F C_ ~P ( A X. B ) /\ ~P ( A X. B ) e. _V ) -> F e. _V )
13	11 12	mpan	|- ( ~P ( A X. B ) e. _V -> F e. _V )
14	2 3 13	3syl	|- ( ( A e. C /\ B e. D ) -> F e. _V )