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

Metamath Proof Explorer

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