Theorem disjx0

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

	Ref	Expression
Assertion	disjx0	⊢ Disj 𝑥 ∈ ∅ 𝐵

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ { ∅ }
2		disjxsn	⊢ Disj 𝑥 ∈ { ∅ } 𝐵
3		disjss1	⊢ ( ∅ ⊆ { ∅ } → ( Disj 𝑥 ∈ { ∅ } 𝐵 → Disj 𝑥 ∈ ∅ 𝐵 ) )
4	1 2 3	mp2	⊢ Disj 𝑥 ∈ ∅ 𝐵