Theorem univ

Description: The union of the universe is the universe. Exercise 4.12(c) of Mendelson p. 235. (Contributed by NM, 14-Sep-2003)

	Ref	Expression
Assertion	univ	⊢ ∪ V = V

Proof

Step	Hyp	Ref	Expression
1		pwv	⊢ 𝒫 V = V
2	1	unieqi	⊢ ∪ 𝒫 V = ∪ V
3		unipw	⊢ ∪ 𝒫 V = V
4	2 3	eqtr3i	⊢ ∪ V = V