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 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶 ) → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		xpexg	⊢ ( ( dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶 ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
2	1	3adant1	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶 ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
3		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
4		relssdmrn	⊢ ( Rel 𝐹 → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
5	3 4	syl	⊢ ( Fun 𝐹 → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
6	5	3ad2ant1	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶 ) → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
7	2 6	ssexd	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶 ) → 𝐹 ∈ V )