Metamath Proof Explorer

Theorem 0disj

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

Ref Expression
Assertion 0disj 
|- Disj_ x e. A (/)

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ { x }
2 1 rgenw 
 |-  A. x e. A (/) C_ { x }
3 sndisj 
 |-  Disj_ x e. A { x }
4 disjss2 
 |-  ( A. x e. A (/) C_ { x } -> ( Disj_ x e. A { x } -> Disj_ x e. A (/) ) )
5 2 3 4 mp2 
 |-  Disj_ x e. A (/)