Metamath Proof Explorer


Theorem imass2

Description: Subset theorem for image. Exercise 22(a) of Enderton p. 53. (Contributed by NM, 22-Mar-1998)

Ref Expression
Assertion imass2 A B C A C B

Proof

Step Hyp Ref Expression
1 ssres2 A B C A C B
2 rnss C A C B ran C A ran C B
3 1 2 syl A B ran C A ran C B
4 df-ima C A = ran C A
5 df-ima C B = ran C B
6 3 4 5 3sstr4g A B C A C B