Metamath Proof Explorer

Theorem mapsspm

Description: Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Assertion mapsspm 
|- ( A ^m B ) C_ ( A ^pm B )

Proof

Step Hyp Ref Expression
1 elmapex 
 |-  ( f e. ( A ^m B ) -> ( A e. _V /\ B e. _V ) )
2 1 simprd 
 |-  ( f e. ( A ^m B ) -> B e. _V )
3 1 simpld 
 |-  ( f e. ( A ^m B ) -> A e. _V )
4 elmapi 
 |-  ( f e. ( A ^m B ) -> f : B --> A )
5 fpmg 
 |-  ( ( B e. _V /\ A e. _V /\ f : B --> A ) -> f e. ( A ^pm B ) )
6 2 3 4 5 syl3anc 
 |-  ( f e. ( A ^m B ) -> f e. ( A ^pm B ) )
7 6 ssriv 
 |-  ( A ^m B ) C_ ( A ^pm B )