Theorem uni0c

Description: The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006)

	Ref	Expression
Assertion	uni0c	⊢ ( ∪ 𝐴 = ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		uni0b	⊢ ( ∪ 𝐴 = ∅ ↔ 𝐴 ⊆ { ∅ } )
2		dfss3	⊢ ( 𝐴 ⊆ { ∅ } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { ∅ } )
3		velsn	⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
4	3	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { ∅ } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )
5	1 2 4	3bitri	⊢ ( ∪ 𝐴 = ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 = ∅ )