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