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

Metamath Proof Explorer

Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Hypothesis axrep4.1 ⊢ Ⅎ 𝑧 𝜑
Assertion axrep4 ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 axrep4.1 ⊢ Ⅎ 𝑧 𝜑
2 ax-rep ⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ∀ 𝑧 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
3 1 19.3 ⊢ ( ∀ 𝑧 𝜑 ↔ 𝜑 )
4 3 imbi1i ⊢ ( ( ∀ 𝑧 𝜑 → 𝑦 = 𝑧 ) ↔ ( 𝜑 → 𝑦 = 𝑧 ) )
5 4 albii ⊢ ( ∀ 𝑦 ( ∀ 𝑧 𝜑 → 𝑦 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
6 5 exbii ⊢ ( ∃ 𝑧 ∀ 𝑦 ( ∀ 𝑧 𝜑 → 𝑦 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
7 6 albii ⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ∀ 𝑧 𝜑 → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
8 3 anbi2i ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
9 8 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
10 9 bibi2i ⊢ ( ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
11 10 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
12 11 exbii ⊢ ( ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
13 2 7 12 3imtr3i ⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )