Metamath Proof Explorer

Theorem disjeq

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

Ref Expression
Assertion disjeq 
|- ( A = B -> ( Disj A <-> Disj B ) )

Proof

Step Hyp Ref Expression
1 eqimss2 
 |-  ( A = B -> B C_ A )
2 1 disjssd 
 |-  ( A = B -> ( Disj A -> Disj B ) )
3 eqimss 
 |-  ( A = B -> A C_ B )
4 3 disjssd 
 |-  ( A = B -> ( Disj B -> Disj A ) )
5 2 4 impbid 
 |-  ( A = B -> ( Disj A <-> Disj B ) )