Theorem uniexg

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. V instead of A e.V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable V . (Contributed by NM, 25-Nov-1994)

	Ref	Expression
Assertion	uniexg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
2	1	eleq1d	$$⊢x=A\to \left(\bigcup x\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}\right)$$
3		vuniex	$$⊢\bigcup x\in \mathrm{V}$$
4	2 3	vtoclg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$