Theorem fabexd

Description: Existence of a set of functions. In contrast to fabex or fabexg , the condition in the class abstraction does not contain the function explicitly, but the function can be derived from it. Therefore, this theorem is also applicable for more special functions like one-to-one, onto or one-to-one onto functions. (Contributed by AV, 20-May-2025)

	Ref	Expression
Hypotheses	fabexd.f	$$⊢\left(\phi \wedge \psi \right)\to f:X⟶Y$$
	fabexd.x	$$⊢\phi \to X\in V$$
	fabexd.y	$$⊢\phi \to Y\in W$$
Assertion	fabexd	$$⊢\phi \to \left\{f|\psi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fabexd.f	$$⊢\left(\phi \wedge \psi \right)\to f:X⟶Y$$
2		fabexd.x	$$⊢\phi \to X\in V$$
3		fabexd.y	$$⊢\phi \to Y\in W$$
4	2 3	xpexd	$$⊢\phi \to X\times Y\in \mathrm{V}$$
5	4	pwexd	$$⊢\phi \to 𝒫\left(X\times Y\right)\in \mathrm{V}$$
6		fssxp	$$⊢f:X⟶Y\to f\subseteq X\times Y$$
7		velpw	$$⊢f\in 𝒫\left(X\times Y\right)\leftrightarrow f\subseteq X\times Y$$
8	6 7	sylibr	$$⊢f:X⟶Y\to f\in 𝒫\left(X\times Y\right)$$
9	1 8	syl	$$⊢\left(\phi \wedge \psi \right)\to f\in 𝒫\left(X\times Y\right)$$
10	9	ex	$$⊢\phi \to \left(\psi \to f\in 𝒫\left(X\times Y\right)\right)$$
11	10	abssdv	$$⊢\phi \to \left\{f|\psi \right\}\subseteq 𝒫\left(X\times Y\right)$$
12	5 11	ssexd	$$⊢\phi \to \left\{f|\psi \right\}\in \mathrm{V}$$