Metamath Proof Explorer

Theorem pmfun

Description: A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion pmfun 
|- ( F e. ( A ^pm B ) -> Fun F )

Proof

Step Hyp Ref Expression
1 elpmi 
 |-  ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )
2 ffun 
 |-  ( F : dom F --> A -> Fun F )
3 2 adantr 
 |-  ( ( F : dom F --> A /\ dom F C_ B ) -> Fun F )
4 1 3 syl 
 |-  ( F e. ( A ^pm B ) -> Fun F )