Theorem fabexg

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

	Ref	Expression
Hypothesis	fabexg.1	$$⊢F=\left\{x|\left(x:A⟶B\wedge \phi \right)\right\}$$
Assertion	fabexg	$$⊢\left(A\in C\wedge B\in D\right)\to F\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fabexg.1	$$⊢F=\left\{x|\left(x:A⟶B\wedge \phi \right)\right\}$$
2		xpexg	$$⊢\left(A\in C\wedge B\in D\right)\to A\times B\in \mathrm{V}$$
3		pwexg	$$⊢A\times B\in \mathrm{V}\to 𝒫\left(A\times B\right)\in \mathrm{V}$$
4		fssxp	$$⊢x:A⟶B\to x\subseteq A\times B$$
5		velpw	$$⊢x\in 𝒫\left(A\times B\right)\leftrightarrow x\subseteq A\times B$$
6	4 5	sylibr	$$⊢x:A⟶B\to x\in 𝒫\left(A\times B\right)$$
7	6	anim1i	$$⊢\left(x:A⟶B\wedge \phi \right)\to \left(x\in 𝒫\left(A\times B\right)\wedge \phi \right)$$
8	7	ss2abi	$$⊢\left\{x|\left(x:A⟶B\wedge \phi \right)\right\}\subseteq \left\{x|\left(x\in 𝒫\left(A\times B\right)\wedge \phi \right)\right\}$$
9	1 8	eqsstri	$$⊢F\subseteq \left\{x|\left(x\in 𝒫\left(A\times B\right)\wedge \phi \right)\right\}$$
10		ssab2	$$⊢\left\{x|\left(x\in 𝒫\left(A\times B\right)\wedge \phi \right)\right\}\subseteq 𝒫\left(A\times B\right)$$
11	9 10	sstri	$$⊢F\subseteq 𝒫\left(A\times B\right)$$
12		ssexg	$$⊢\left(F\subseteq 𝒫\left(A\times B\right)\wedge 𝒫\left(A\times B\right)\in \mathrm{V}\right)\to F\in \mathrm{V}$$
13	11 12	mpan	$$⊢𝒫\left(A\times B\right)\in \mathrm{V}\to F\in \mathrm{V}$$
14	2 3 13	3syl	$$⊢\left(A\in C\wedge B\in D\right)\to F\in \mathrm{V}$$