Metamath Proof Explorer

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 V A V


Step Hyp Ref Expression
1 unieq x = A x = A
2 1 eleq1d x = A x V A V
3 vuniex x V
4 2 3 vtoclg A V A V