Theorem fex2

Description: A function with bounded domain and codomain is a set. This version of fex is proven without the Axiom of Replacement ax-rep , but depends on ax-un , which is not required for the proof of fex . (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	fex2	$$⊢\left(F:A⟶B\wedge A\in V\wedge B\in W\right)\to F\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		xpexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\times B\in \mathrm{V}$$
2	1	3adant1	$$⊢\left(F:A⟶B\wedge A\in V\wedge B\in W\right)\to A\times B\in \mathrm{V}$$
3		fssxp	$$⊢F:A⟶B\to F\subseteq A\times B$$
4	3	3ad2ant1	$$⊢\left(F:A⟶B\wedge A\in V\wedge B\in W\right)\to F\subseteq A\times B$$
5	2 4	ssexd	$$⊢\left(F:A⟶B\wedge A\in V\wedge B\in W\right)\to F\in \mathrm{V}$$