Theorem axrep2 2690

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on φ.

Assertion

Ref	Expression
axrep2	⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))

Distinct variable group:   x,y,z

Proof of Theorem axrep2

Step	Hyp	Ref	Expression
1		hbe1 1014	. . . . 5 ⊢ (∃w∀z(∀yφ → z = w) → ∀w∃w∀z(∀yφ → z = w))
2		ax-17 969	. . . . 5 ⊢ (∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)) → ∀w∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))
3	1, 2	hbim 1005	. . . 4 ⊢ ((∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) → ∀w(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
4	3	hbex 1004	. . 3 ⊢ (∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) → ∀w∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
5		elequ2 1135	. . . . . . . . 9 ⊢ (w = y → (x ∈ w ↔ x ∈ y))
6	5	anbi1d 616	. . . . . . . 8 ⊢ (w = y → ((x ∈ w ⋀ ∀yφ) ↔ (x ∈ y ⋀ ∀yφ)))
7	6	exbidv 1277	. . . . . . 7 ⊢ (w = y → (∃x(x ∈ w ⋀ ∀yφ) ↔ ∃x(x ∈ y ⋀ ∀yφ)))
8	7	bibi2d 617	. . . . . 6 ⊢ (w = y → ((z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ (z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
9	8	albidv 1276	. . . . 5 ⊢ (w = y → (∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
10	9	imbi2d 611	. . . 4 ⊢ (w = y → ((∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ))) ↔ (∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))))
11	10	exbidv 1277	. . 3 ⊢ (w = y → (∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ))) ↔ ∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))))
12		axrep1 2689	. . 3 ⊢ ∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)))
13	4, 11, 12	chvar 1165	. 2 ⊢ ∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))
14		ax-4 971	. . . . . . . 8 ⊢ (∀yφ → φ)
15	14	imim1i 16	. . . . . . 7 ⊢ ((φ → z = y) → (∀yφ → z = y))
16	15	19.20i 990	. . . . . 6 ⊢ (∀z(φ → z = y) → ∀z(∀yφ → z = y))
17	16	19.22i 1038	. . . . 5 ⊢ (∃y∀z(φ → z = y) → ∃y∀z(∀yφ → z = y))
18		ax-17 969	. . . . . 6 ⊢ (∀z(∀yφ → z = y) → ∀w∀z(∀yφ → z = y))
19		hba1 1001	. . . . . . . 8 ⊢ (∀yφ → ∀y∀yφ)
20		ax-17 969	. . . . . . . 8 ⊢ (z = w → ∀y z = w)
21	19, 20	hbim 1005	. . . . . . 7 ⊢ ((∀yφ → z = w) → ∀y(∀yφ → z = w))
22	21	hbal 1003	. . . . . 6 ⊢ (∀z(∀yφ → z = w) → ∀y∀z(∀yφ → z = w))
23		equequ2 1133	. . . . . . . 8 ⊢ (y = w → (z = y ↔ z = w))
24	23	imbi2d 611	. . . . . . 7 ⊢ (y = w → ((∀yφ → z = y) ↔ (∀yφ → z = w)))
25	24	albidv 1276	. . . . . 6 ⊢ (y = w → (∀z(∀yφ → z = y) ↔ ∀z(∀yφ → z = w)))
26	18, 22, 25	cbvex 1164	. . . . 5 ⊢ (∃y∀z(∀yφ → z = y) ↔ ∃w∀z(∀yφ → z = w))
27	17, 26	sylib 198	. . . 4 ⊢ (∃y∀z(φ → z = y) → ∃w∀z(∀yφ → z = w))
28	27	imim1i 16	. . 3 ⊢ ((∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) → (∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
29	28	19.22i 1038	. 2 ⊢ (∃x(∃w∀z(∀yφ → z = w) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
30	13, 29	ax-mp 7	1 ⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978

This theorem is referenced by:  axrep3 2691  axrepndlem1 4924

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-rep 2688

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain