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

Metamath Proof Explorer

Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003) Shorten proof and reduce axiom dependencies. (Revised by BJ, 5-Apr-2026)

Ref Expression
Assertion zfrep6 
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )

Proof

Step Hyp Ref Expression
1 euex 
 |-  ( E! y ph -> E. y ph )
2 1 ralimi 
 |-  ( A. x e. z E! y ph -> A. x e. z E. y ph )
3 df-ral 
 |-  ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) )
4 eumo 
 |-  ( E! y ph -> E* y ph )
5 4 imim2i 
 |-  ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) )
6 moanimv 
 |-  ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) )
7 5 6 sylibr 
 |-  ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) )
8 7 alimi 
 |-  ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) )
9 3 8 sylbi 
 |-  ( A. x e. z E! y ph -> A. x E* y ( x e. z /\ ph ) )
10 axrep6 
 |-  ( A. x E* y ( x e. z /\ ph ) -> E. w A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) )
11 rexanid 
 |-  ( E. x e. z ( x e. z /\ ph ) <-> E. x e. z ph )
12 11 bibi2i 
 |-  ( ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> ( y e. w <-> E. x e. z ph ) )
13 12 albii 
 |-  ( A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> A. y ( y e. w <-> E. x e. z ph ) )
14 13 exbii 
 |-  ( E. w A. y ( y e. w <-> E. x e. z ( x e. z /\ ph ) ) <-> E. w A. y ( y e. w <-> E. x e. z ph ) )
15 10 14 sylib 
 |-  ( A. x E* y ( x e. z /\ ph ) -> E. w A. y ( y e. w <-> E. x e. z ph ) )
16 9 15 syl 
 |-  ( A. x e. z E! y ph -> E. w A. y ( y e. w <-> E. x e. z ph ) )
17 replem 
 |-  ( ( A. x e. z E. y ph /\ E. w A. y ( y e. w <-> E. x e. z ph ) ) -> E. w A. x e. z E. y e. w ph )
18 2 16 17 syl2anc 
 |-  ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )