Metamath Proof Explorer

Theorem fpmg

Description: A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Assertion fpmg 
|- ( ( A e. V /\ B e. W /\ F : A --> B ) -> F e. ( B ^pm A ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  A C_ A
2 elpm2r 
 |-  ( ( ( B e. W /\ A e. V ) /\ ( F : A --> B /\ A C_ A ) ) -> F e. ( B ^pm A ) )
3 1 2 mpanr2 
 |-  ( ( ( B e. W /\ A e. V ) /\ F : A --> B ) -> F e. ( B ^pm A ) )
4 3 3impa 
 |-  ( ( B e. W /\ A e. V /\ F : A --> B ) -> F e. ( B ^pm A ) )
5 4 3com12 
 |-  ( ( A e. V /\ B e. W /\ F : A --> B ) -> F e. ( B ^pm A ) )