Metamath Proof Explorer

Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994)

Ref Expression
Hypothesis axrep4.1 ⊢Ⅎzφ
Assertion axrep4 ⊢∀x∃z∀yφ→y=z→∃z∀yy∈z↔∃xx∈w∧φ

Proof

Step Hyp Ref Expression
1 axrep4.1 ⊢Ⅎzφ
2 axrep3 ⊢∃x∃z∀yφ→y=z→∀yy∈x↔∃xx∈w∧∀zφ
3 2 19.35i ⊢∀x∃z∀yφ→y=z→∃x∀yy∈x↔∃xx∈w∧∀zφ
4 nfv ⊢Ⅎzy∈x
5 nfv ⊢Ⅎzx∈w
6 nfa1 ⊢Ⅎz∀zφ
7 5 6 nfan ⊢Ⅎzx∈w∧∀zφ
8 7 nfex ⊢Ⅎz∃xx∈w∧∀zφ
9 4 8 nfbi ⊢Ⅎzy∈x↔∃xx∈w∧∀zφ
10 9 nfal ⊢Ⅎz∀yy∈x↔∃xx∈w∧∀zφ
11 nfv ⊢Ⅎxy∈z
12 nfe1 ⊢Ⅎx∃xx∈w∧φ
13 11 12 nfbi ⊢Ⅎxy∈z↔∃xx∈w∧φ
14 13 nfal ⊢Ⅎx∀yy∈z↔∃xx∈w∧φ
15 elequ2 ⊢x=z→y∈x↔y∈z
16 1 19.3 ⊢∀zφ↔φ
17 16 anbi2i ⊢x∈w∧∀zφ↔x∈w∧φ
18 17 exbii ⊢∃xx∈w∧∀zφ↔∃xx∈w∧φ
19 18 a1i ⊢x=z→∃xx∈w∧∀zφ↔∃xx∈w∧φ
20 15 19 bibi12d ⊢x=z→y∈x↔∃xx∈w∧∀zφ↔y∈z↔∃xx∈w∧φ
21 20 albidv ⊢x=z→∀yy∈x↔∃xx∈w∧∀zφ↔∀yy∈z↔∃xx∈w∧φ
22 10 14 21 cbvexv1 ⊢∃x∀yy∈x↔∃xx∈w∧∀zφ↔∃z∀yy∈z↔∃xx∈w∧φ
23 3 22 sylib ⊢∀x∃z∀yφ→y=z→∃z∀yy∈z↔∃xx∈w∧φ