Metamath Proof Explorer

Theorem disjx0

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

Ref Expression
Assertion disjx0 
|- Disj_ x e. (/) B

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ { (/) }
2 disjxsn 
 |-  Disj_ x e. { (/) } B
3 disjss1 
 |-  ( (/) C_ { (/) } -> ( Disj_ x e. { (/) } B -> Disj_ x e. (/) B ) )
4 1 2 3 mp2 
 |-  Disj_ x e. (/) B