Metamath Proof Explorer


Theorem disjeq0

Description: Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion disjeq0 A B = A = B A = B =

Proof

Step Hyp Ref Expression
1 ineq1 A = B A B = B B
2 inidm B B = B
3 1 2 eqtrdi A = B A B = B
4 3 eqeq1d A = B A B = B =
5 eqtr A = B B = A =
6 simpr A = B B = B =
7 5 6 jca A = B B = A = B =
8 7 ex A = B B = A = B =
9 4 8 sylbid A = B A B = A = B =
10 9 com12 A B = A = B A = B =
11 eqtr3 A = B = A = B
12 10 11 impbid1 A B = A = B A = B =