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	|- ( A. x e. z E. y ph -> E. w A. x e. z E. y e. w ph )

Proof

Step	Hyp	Ref	Expression
1		cp	|- E. w A. x e. z ( E. y ph -> E. y e. w ph )
2		ralim	|- ( A. x e. z ( E. y ph -> E. y e. w ph ) -> ( A. x e. z E. y ph -> A. x e. z E. y e. w ph ) )
3	1 2	eximii	|- E. w ( A. x e. z E. y ph -> A. x e. z E. y e. w ph )
4	3	19.37iv	|- ( A. x e. z E. y ph -> E. w A. x e. z E. y e. w ph )