Theorem ioofun

Description: (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Assertion	ioofun	$$⊢\mathrm{Fun}\left(.\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioof	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ$$
2		ffun	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ\to \mathrm{Fun}\left(.\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\left(.\right)$$