Theorem disjssi

Description: Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021)

	Ref	Expression
Hypothesis	disjssi.1	$$⊢A\subseteq B$$
Assertion	disjssi	$$⊢DisjB\to DisjA$$

Proof

Step	Hyp	Ref	Expression
1		disjssi.1	$$⊢A\subseteq B$$
2		disjss	$$⊢A\subseteq B\to \left(DisjB\to DisjA\right)$$
3	1 2	ax-mp	$$⊢DisjB\to DisjA$$