Metamath Proof Explorer

Theorem funexw

Description: Weak version of funex that holds without ax-rep . If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Assertion	funexw	$⊢ (Fun F \land dom F \in B \land ran F \in C) \to F \in V$

Proof

Step	Hyp	Ref	Expression
1		xpexg	$⊢ (dom F \in B \land ran F \in C) \to dom F \times ran F \in V$
2	1	3adant1	$⊢ (Fun F \land dom F \in B \land ran F \in C) \to dom F \times ran F \in V$
3		funrel	$⊢ Fun F \to Rel F$
4		relssdmrn	$⊢ Rel F \to F \subseteq dom F \times ran F$
5	3 4	syl	$⊢ Fun F \to F \subseteq dom F \times ran F$
6	5	3ad2ant1	$⊢ (Fun F \land dom F \in B \land ran F \in C) \to F \subseteq dom F \times ran F$
7	2 6	ssexd	$⊢ (Fun F \land dom F \in B \land ran F \in C) \to F \in V$