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	⊢ ( 𝐴 ↑m 𝐵 ) ⊆ ( 𝐴 ↑pm 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elmapex	⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
2	1	simprd	⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) → 𝐵 ∈ V )
3	1	simpld	⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) → 𝐴 ∈ V )
4		elmapi	⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) → 𝑓 : 𝐵 ⟶ 𝐴 )
5		fpmg	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) )
6	2 3 4 5	syl3anc	⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) → 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) )
7	6	ssriv	⊢ ( 𝐴 ↑m 𝐵 ) ⊆ ( 𝐴 ↑pm 𝐵 )