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

Metamath Proof Explorer

Theorem bnd

Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 ), derived from the Collection Principle cp . Its strength lies in the rather profound fact that ph ( x , y ) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. (Contributed by NM, 17-Oct-2004)

		Ref	Expression
	Assertion	bnd	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		cp	⊢ ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 )
2		ralim	⊢ ( ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ) )
3	1 2	eximii	⊢ ∃ 𝑤 ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )
4	3	19.37iv	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )