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 ⊢ ∀ x ∈ z ∃ y φ → ∃ w ∀ x ∈ z ∃ y ∈ w φ

Proof

Step Hyp Ref Expression
1 cp ⊢ ∃ w ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ
2 ralim ⊢ ∀ x ∈ z ∃ y φ → ∃ y ∈ w φ → ∀ x ∈ z ∃ y φ → ∀ x ∈ z ∃ y ∈ w φ
3 1 2 eximii ⊢ ∃ w ∀ x ∈ z ∃ y φ → ∀ x ∈ z ∃ y ∈ w φ
4 3 19.37iv ⊢ ∀ x ∈ z ∃ y φ → ∃ w ∀ x ∈ z ∃ y ∈ w φ