This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		unieq	⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
2	1	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V ) )
3		vuniex	⊢ ∪ 𝑥 ∈ V
4	2 3	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )