This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqabb 
 |-  ( 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