Theorem axrep5

Description: Axiom of Replacement (similar to Axiom Rep of BellMachover p. 463). The antecedent tells us ph is analogous to a "function" from x to y (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set z that corresponds to the "image" of ph restricted to some other set w . The hypothesis says z must not be free in ph . (Contributed by NM, 26-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypothesis	axrep5.1	|- F/ z ph
Assertion	axrep5	|- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		axrep5.1	|- F/ z ph
2		19.37v	|- ( E. z ( x e. w -> A. y ( ph -> y = z ) ) <-> ( x e. w -> E. z A. y ( ph -> y = z ) ) )
3		impexp	|- ( ( ( x e. w /\ ph ) -> y = z ) <-> ( x e. w -> ( ph -> y = z ) ) )
4	3	albii	|- ( A. y ( ( x e. w /\ ph ) -> y = z ) <-> A. y ( x e. w -> ( ph -> y = z ) ) )
5		19.21v	|- ( A. y ( x e. w -> ( ph -> y = z ) ) <-> ( x e. w -> A. y ( ph -> y = z ) ) )
6	4 5	bitr2i	|- ( ( x e. w -> A. y ( ph -> y = z ) ) <-> A. y ( ( x e. w /\ ph ) -> y = z ) )
7	6	exbii	|- ( E. z ( x e. w -> A. y ( ph -> y = z ) ) <-> E. z A. y ( ( x e. w /\ ph ) -> y = z ) )
8	2 7	bitr3i	|- ( ( x e. w -> E. z A. y ( ph -> y = z ) ) <-> E. z A. y ( ( x e. w /\ ph ) -> y = z ) )
9	8	albii	|- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) <-> A. x E. z A. y ( ( x e. w /\ ph ) -> y = z ) )
10		nfv	|- F/ z x e. w
11	10 1	nfan	|- F/ z ( x e. w /\ ph )
12	11	axrep4	|- ( A. x E. z A. y ( ( x e. w /\ ph ) -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ( x e. w /\ ph ) ) ) )
13	9 12	sylbi	|- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ( x e. w /\ ph ) ) ) )
14		anabs5	|- ( ( x e. w /\ ( x e. w /\ ph ) ) <-> ( x e. w /\ ph ) )
15	14	exbii	|- ( E. x ( x e. w /\ ( x e. w /\ ph ) ) <-> E. x ( x e. w /\ ph ) )
16	15	bibi2i	|- ( ( y e. z <-> E. x ( x e. w /\ ( x e. w /\ ph ) ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) )
17	16	albii	|- ( A. y ( y e. z <-> E. x ( x e. w /\ ( x e. w /\ ph ) ) ) <-> A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
18	17	exbii	|- ( E. z A. y ( y e. z <-> E. x ( x e. w /\ ( x e. w /\ ph ) ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
19	13 18	sylib	|- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )