Theorem ioofun

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

	Ref	Expression
Assertion	ioofun	⊢ Fun (,)

Proof

Step	Hyp	Ref	Expression
1		ioof	⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
2		ffun	⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
3	1 2	ax-mp	⊢ Fun (,)