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 B x A C x B C


Step Hyp Ref Expression
1 ssel A B x A x B
2 1 anim1d A B x A y = C x B y = C
3 2 ssopab2dv A B x y | x A y = C x y | x B y = C
4 df-mpt x A C = x y | x A y = C
5 df-mpt x B C = x y | x B y = C
6 3 4 5 3sstr4g A B x A C x B C