This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imass2d

Description: Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	imass2d.1	$⊢ φ \to A \subseteq B$
	Assertion	imass2d	$⊢ φ \to C [A] \subseteq C [B]$

Step	Hyp	Ref	Expression
1		imass2d.1	$⊢ φ \to A \subseteq B$
2		imass2	$⊢ A \subseteq B \to C [A] \subseteq C [B]$
3	1 2	syl	$⊢ φ \to C [A] \subseteq C [B]$