Metamath Proof Explorer

Theorem fpm

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

Ref Expression
Hypotheses elmap.1 
|- A e. _V
elmap.2 
|- B e. _V
Assertion fpm 
|- ( F : A --> B -> F e. ( B ^pm A ) )

Proof

Step Hyp Ref Expression
1 elmap.1 
 |-  A e. _V
2 elmap.2 
 |-  B e. _V
3 fpmg 
 |-  ( ( A e. _V /\ B e. _V /\ F : A --> B ) -> F e. ( B ^pm A ) )
4 1 2 3 mp3an12 
 |-  ( F : A --> B -> F e. ( B ^pm A ) )