Theorem disjeqi

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

	Ref	Expression
Hypothesis	disjeqi.1	$$⊢A=B$$
Assertion	disjeqi	$$⊢DisjA\leftrightarrow DisjB$$

Proof

Step	Hyp	Ref	Expression
1		disjeqi.1	$$⊢A=B$$
2		disjeq	$$⊢A=B\to \left(DisjA\leftrightarrow DisjB\right)$$
3	1 2	ax-mp	$$⊢DisjA\leftrightarrow DisjB$$