Metamath Proof Explorer

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 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
2 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
3 1 2 ax-mp 
 |-  Fun (,)