axrep2

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph . (Contributed by NM, 15-Aug-2003) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

		Ref	Expression
	Assertion	axrep2	⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfe1	⊢ Ⅎ 𝑤 ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 )
2		nfv	⊢ Ⅎ 𝑤 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) )
3	1 2	nfim	⊢ Ⅎ 𝑤 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
4	3	nfex	⊢ Ⅎ 𝑤 ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
5		axreplem	⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
6		axrep1	⊢ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 𝜑 ) ) )
7	4 5 6	chvarfv	⊢ ∃ 𝑥 ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
8		sp	⊢ ( ∀ 𝑦 𝜑 → 𝜑 )
9	8	imim1i	⊢ ( ( 𝜑 → 𝑧 = 𝑦 ) → ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
10	9	alimi	⊢ ( ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
11	10	eximi	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) )
12		nfv	⊢ Ⅎ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 )
13		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
14		nfv	⊢ Ⅎ 𝑦 𝑧 = 𝑤
15	13 14	nfim	⊢ Ⅎ 𝑦 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 )
16	15	nfal	⊢ Ⅎ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 )
17		equequ2	⊢ ( 𝑦 = 𝑤 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝑤 ) )
18	17	imbi2d	⊢ ( 𝑦 = 𝑤 → ( ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) )
19	18	albidv	⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) ) )
20	12 16 19	cbvexv1	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) )
21	11 20	sylib	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) )
22	21	imim1i	⊢ ( ( ∃ 𝑤 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑤 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) → ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
23	7 22	eximii	⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )

Metamath Proof Explorer

Theorem axrep2

Proof