Theorem disjeq

Description: Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021)

	Ref	Expression
Assertion	disjeq	$$⊢A=B\to \left(DisjA\leftrightarrow DisjB\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2	1	disjssd	$$⊢A=B\to \left(DisjA\to DisjB\right)$$
3		eqimss	$$⊢A=B\to A\subseteq B$$
4	3	disjssd	$$⊢A=B\to \left(DisjB\to DisjA\right)$$
5	2 4	impbid	$$⊢A=B\to \left(DisjA\leftrightarrow DisjB\right)$$