cossss

Description: Subclass theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 11-Nov-2019)

		Ref	Expression
	Assertion	cossss	$⊢ A \subseteq B \to ≀ A \subseteq ≀ B$

Step	Hyp	Ref	Expression
1		ssbr	$⊢ A \subseteq B \to (x A y \to x B y)$
2		ssbr	$⊢ A \subseteq B \to (x A z \to x B z)$
3	1 2	anim12d	$⊢ A \subseteq B \to ((x A y \land x A z) \to (x B y \land x B z))$
4	3	eximdv	$⊢ A \subseteq B \to (\exists x (x A y \land x A z) \to \exists x (x B y \land x B z))$
5	4	ssopab2dv	$⊢ A \subseteq B \to \{⟨y, z⟩ \| \exists x (x A y \land x A z)\} \subseteq \{⟨y, z⟩ \| \exists x (x B y \land x B z)\}$
6		df-coss	$⊢ ≀ A = \{⟨y, z⟩ \| \exists x (x A y \land x A z)\}$
7		df-coss	$⊢ ≀ B = \{⟨y, z⟩ \| \exists x (x B y \land x B z)\}$
8	5 6 7	3sstr4g	$⊢ A \subseteq B \to ≀ A \subseteq ≀ B$

Metamath Proof Explorer