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	$$⊢\forall x\in z\exists y\phi \to \exists w\forall x\in z\exists y\in w\phi$$

Proof

Step	Hyp	Ref	Expression
1		cp	$$⊢\exists w\forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)$$
2		ralim	$$⊢\forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)\to \left(\forall x\in z\exists y\phi \to \forall x\in z\exists y\in w\phi \right)$$
3	1 2	eximii	$$⊢\exists w\left(\forall x\in z\exists y\phi \to \forall x\in z\exists y\in w\phi \right)$$
4	3	19.37iv	$$⊢\forall x\in z\exists y\phi \to \exists w\forall x\in z\exists y\in w\phi$$