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 ⊢ Ⅎ 𝑧 𝜑
Assertion axrep5 ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )

Proof

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