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 /\ dom F e. B /\ ran F e. C ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		xpexg	|- ( ( dom F e. B /\ ran F e. C ) -> ( dom F X. ran F ) e. _V )
2	1	3adant1	|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> ( dom F X. ran F ) e. _V )
3		funrel	|- ( Fun F -> Rel F )
4		relssdmrn	|- ( Rel F -> F C_ ( dom F X. ran F ) )
5	3 4	syl	|- ( Fun F -> F C_ ( dom F X. ran F ) )
6	5	3ad2ant1	|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F C_ ( dom F X. ran F ) )
7	2 6	ssexd	|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F e. _V )