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

Metamath Proof Explorer

Theorem disjeq

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

		Ref	Expression
	Assertion	disjeq	$⊢ A = B \to (Disj A \leftrightarrow Disj B)$

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