Metamath Proof Explorer

Theorem fex2

Description: A function with bounded domain and range is a set. This version of fex is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	fex2	$⊢ (F : A ⟶ B \land A \in V \land B \in W) \to F \in V$

Proof

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