Theorem unisn0

Description: The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	unisn0	⊢ ∪ { ∅ } = ∅

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ { ∅ } ⊆ { ∅ }
2		uni0b	⊢ ( ∪ { ∅ } = ∅ ↔ { ∅ } ⊆ { ∅ } )
3	1 2	mpbir	⊢ ∪ { ∅ } = ∅