Metamath Proof Explorer


Theorem disjeqd

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

Ref Expression
Hypothesis disjeqd.1 φ A = B
Assertion disjeqd φ Disj A Disj B

Proof

Step Hyp Ref Expression
1 disjeqd.1 φ A = B
2 disjeq A = B Disj A Disj B
3 1 2 syl φ Disj A Disj B