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	$$⊢\bigcup \mathrm{V}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		pwv	$$⊢𝒫\mathrm{V}=\mathrm{V}$$
2	1	unieqi	$$⊢\bigcup 𝒫\mathrm{V}=\bigcup \mathrm{V}$$
3		unipw	$$⊢\bigcup 𝒫\mathrm{V}=\mathrm{V}$$
4	2 3	eqtr3i	$$⊢\bigcup \mathrm{V}=\mathrm{V}$$