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

Metamath Proof Explorer

Theorem axun2

Description: A variant of the Axiom of Union ax-un . For any set x , there exists a set y whose members are exactly the members of the members of x i.e. the union of x . Axiom Union of BellMachover p. 466. (Contributed by NM, 4-Jun-2006)

		Ref	Expression
	Assertion	axun2	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-un	⊢ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
2	1	sepexi	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )