Metamath Proof Explorer


Theorem 0disj

Description: Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion 0disj DisjxA

Proof

Step Hyp Ref Expression
1 0ss x
2 1 rgenw xAx
3 sndisj DisjxAx
4 disjss2 xAxDisjxAxDisjxA
5 2 3 4 mp2 DisjxA