Theorem zfrepclf

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	zfrepclf.1	|- F/_ x A
	zfrepclf.2	|- A e. _V
	zfrepclf.3	|- ( x e. A -> E. z A. y ( ph -> y = z ) )
Assertion	zfrepclf	|- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		zfrepclf.1	|- F/_ x A
2		zfrepclf.2	|- A e. _V
3		zfrepclf.3	|- ( x e. A -> E. z A. y ( ph -> y = z ) )
4	1	nfeq2	|- F/ x v = A
5		eleq2	|- ( v = A -> ( x e. v <-> x e. A ) )
6	5 3	biimtrdi	|- ( v = A -> ( x e. v -> E. z A. y ( ph -> y = z ) ) )
7	4 6	alrimi	|- ( v = A -> A. x ( x e. v -> E. z A. y ( ph -> y = z ) ) )
8		nfv	|- F/ z ph
9	8	axrep5	|- ( A. x ( x e. v -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. v /\ ph ) ) )
10	7 9	syl	|- ( v = A -> E. z A. y ( y e. z <-> E. x ( x e. v /\ ph ) ) )
11	5	anbi1d	|- ( v = A -> ( ( x e. v /\ ph ) <-> ( x e. A /\ ph ) ) )
12	4 11	exbid	|- ( v = A -> ( E. x ( x e. v /\ ph ) <-> E. x ( x e. A /\ ph ) ) )
13	12	bibi2d	|- ( v = A -> ( ( y e. z <-> E. x ( x e. v /\ ph ) ) <-> ( y e. z <-> E. x ( x e. A /\ ph ) ) ) )
14	13	albidv	|- ( v = A -> ( A. y ( y e. z <-> E. x ( x e. v /\ ph ) ) <-> A. y ( y e. z <-> E. x ( x e. A /\ ph ) ) ) )
15	14	exbidv	|- ( v = A -> ( E. z A. y ( y e. z <-> E. x ( x e. v /\ ph ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) ) ) )
16	10 15	mpbid	|- ( v = A -> E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) ) )
17	2 16	vtocle	|- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )