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	\|- ( 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 )