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 e. V -> U. A e. _V )

Proof

Step	Hyp	Ref	Expression
1		unieq	|- ( x = A -> U. x = U. A )
2	1	eleq1d	|- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vuniex	|- U. x e. _V
4	2 3	vtoclg	|- ( A e. V -> U. A e. _V )