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 ABxACxBC

Proof

Step Hyp Ref Expression
1 ssel ABxAxB
2 1 anim1d ABxAy=CxBy=C
3 2 ssopab2dv ABxy|xAy=Cxy|xBy=C
4 df-mpt xAC=xy|xAy=C
5 df-mpt xBC=xy|xBy=C
6 3 4 5 3sstr4g ABxACxBC