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 ⊢ ∀ x x ∈ w → ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ

Proof

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