Metamath Proof Explorer

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 ⊢Ⅎzφ
Assertion axrep5 ⊢∀xx∈w→∃z∀yφ→y=z→∃z∀yy∈z↔∃xx∈w∧φ

Proof

Step Hyp Ref Expression
1 axrep5.1 ⊢Ⅎzφ
2 19.37v ⊢∃zx∈w→∀yφ→y=z↔x∈w→∃z∀yφ→y=z
3 impexp ⊢x∈w∧φ→y=z↔x∈w→φ→y=z
4 3 albii ⊢∀yx∈w∧φ→y=z↔∀yx∈w→φ→y=z
5 19.21v ⊢∀yx∈w→φ→y=z↔x∈w→∀yφ→y=z
6 4 5 bitr2i ⊢x∈w→∀yφ→y=z↔∀yx∈w∧φ→y=z
7 6 exbii ⊢∃zx∈w→∀yφ→y=z↔∃z∀yx∈w∧φ→y=z
8 2 7 bitr3i ⊢x∈w→∃z∀yφ→y=z↔∃z∀yx∈w∧φ→y=z
9 8 albii ⊢∀xx∈w→∃z∀yφ→y=z↔∀x∃z∀yx∈w∧φ→y=z
10 nfv ⊢Ⅎzx∈w
11 10 1 nfan ⊢Ⅎzx∈w∧φ
12 11 axrep4 ⊢∀x∃z∀yx∈w∧φ→y=z→∃z∀yy∈z↔∃xx∈w∧x∈w∧φ
13 9 12 sylbi ⊢∀xx∈w→∃z∀yφ→y=z→∃z∀yy∈z↔∃xx∈w∧x∈w∧φ
14 anabs5 ⊢x∈w∧x∈w∧φ↔x∈w∧φ
15 14 exbii ⊢∃xx∈w∧x∈w∧φ↔∃xx∈w∧φ
16 15 bibi2i ⊢y∈z↔∃xx∈w∧x∈w∧φ↔y∈z↔∃xx∈w∧φ
17 16 albii ⊢∀yy∈z↔∃xx∈w∧x∈w∧φ↔∀yy∈z↔∃xx∈w∧φ
18 17 exbii ⊢∃z∀yy∈z↔∃xx∈w∧x∈w∧φ↔∃z∀yy∈z↔∃xx∈w∧φ
19 13 18 sylib ⊢∀xx∈w→∃z∀yφ→y=z→∃z∀yy∈z↔∃xx∈w∧φ