Theorem zfrep4

Description: A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Hypotheses	zfrep4.1	|- { x | ph } e. _V
	zfrep4.2	|- ( ph -> E. z A. y ( ps -> y = z ) )
Assertion	zfrep4	|- { y | E. x ( ph /\ ps ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		zfrep4.1	|- { x | ph } e. _V
2		zfrep4.2	|- ( ph -> E. z A. y ( ps -> y = z ) )
3		abid	|- ( x e. { x | ph } <-> ph )
4	3	anbi1i	|- ( ( x e. { x | ph } /\ ps ) <-> ( ph /\ ps ) )
5	4	exbii	|- ( E. x ( x e. { x | ph } /\ ps ) <-> E. x ( ph /\ ps ) )
6	5	abbii	|- { y | E. x ( x e. { x | ph } /\ ps ) } = { y | E. x ( ph /\ ps ) }
7		nfab1	|- F/_ x { x | ph }
8	3 2	sylbi	|- ( x e. { x | ph } -> E. z A. y ( ps -> y = z ) )
9	7 1 8	zfrepclf	|- E. z A. y ( y e. z <-> E. x ( x e. { x | ph } /\ ps ) )
10		abeq2	|- ( z = { y | E. x ( x e. { x | ph } /\ ps ) } <-> A. y ( y e. z <-> E. x ( x e. { x | ph } /\ ps ) ) )
11	10	exbii	|- ( E. z z = { y | E. x ( x e. { x | ph } /\ ps ) } <-> E. z A. y ( y e. z <-> E. x ( x e. { x | ph } /\ ps ) ) )
12	9 11	mpbir	|- E. z z = { y | E. x ( x e. { x | ph } /\ ps ) }
13	12	issetri	|- { y | E. x ( x e. { x | ph } /\ ps ) } e. _V
14	6 13	eqeltrri	|- { y | E. x ( ph /\ ps ) } e. _V