Theorem zfrep3cl

Description: An inference based on the Axiom of Replacement. Typically, ph defines a function from x to y . (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Hypotheses	zfrep3cl.1	|- A e. _V
	zfrep3cl.2	|- ( x e. A -> E. z A. y ( ph -> y = z ) )
Assertion	zfrep3cl	|- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		zfrep3cl.1	|- A e. _V
2		zfrep3cl.2	|- ( x e. A -> E. z A. y ( ph -> y = z ) )
3		nfcv	|- F/_ x A
4	3 1 2	zfrepclf	|- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )