Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994)

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

Proof

Step	Hyp	Ref	Expression
1		axrep4.1	⊢ Ⅎ 𝑧 𝜑
2		axrep3	⊢ ∃ 𝑥 ( ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
3	2	19.35i	⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
4		nfv	⊢ Ⅎ 𝑧 𝑦 ∈ 𝑥
5		nfv	⊢ Ⅎ 𝑧 𝑥 ∈ 𝑤
6		nfa1	⊢ Ⅎ 𝑧 ∀ 𝑧 𝜑
7	5 6	nfan	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 )
8	7	nfex	⊢ Ⅎ 𝑧 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 )
9	4 8	nfbi	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) )
10	9	nfal	⊢ Ⅎ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) )
11		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑧
12		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 )
13	11 12	nfbi	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
14	13	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
15		elequ2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 ) )
16	1	19.3	⊢ ( ∀ 𝑧 𝜑 ↔ 𝜑 )
17	16	anbi2i	⊢ ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
18	17	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
19	18	a1i	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
20	15 19	bibi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
21	20	albidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ) )
22	10 14 21	cbvexv1	⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
23	3 22	sylib	⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )