# Metamath Proof Explorer

## Theorem mptssALT

Description: Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss . (Contributed by Thierry Arnoux, 30-May-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mptssALT ${⊢}{A}\subseteq {B}\to \left({x}\in {A}⟼{C}\right)\subseteq \left({x}\in {B}⟼{C}\right)$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {B}\to \left({x}\in {A}\to {x}\in {B}\right)$
2 1 anim1d ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {A}\wedge {y}={C}\right)\to \left({x}\in {B}\wedge {y}={C}\right)\right)$
3 2 ssopab2dv ${⊢}{A}\subseteq {B}\to \left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={C}\right)\right\}\subseteq \left\{⟨{x},{y}⟩|\left({x}\in {B}\wedge {y}={C}\right)\right\}$
4 df-mpt ${⊢}\left({x}\in {A}⟼{C}\right)=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}={C}\right)\right\}$
5 df-mpt ${⊢}\left({x}\in {B}⟼{C}\right)=\left\{⟨{x},{y}⟩|\left({x}\in {B}\wedge {y}={C}\right)\right\}$
6 3 4 5 3sstr4g ${⊢}{A}\subseteq {B}\to \left({x}\in {A}⟼{C}\right)\subseteq \left({x}\in {B}⟼{C}\right)$