Theorem axrep1 2690

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 2689 → axrep1 2690 → axrep2 2691 → axrepnd 4938 → zfcndrep 4958 = ax-rep 2689.

Assertion

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

Distinct variable groups:   φ,y   x,y,z

Proof of Theorem axrep1

Step	Hyp	Ref	Expression
1		elequ2 1135	. . . . . . . . . 10 ⊢ (w = y → (x ∈ w ↔ x ∈ y))
2	1	anbi1d 616	. . . . . . . . 9 ⊢ (w = y → ((x ∈ w ⋀ ∀yφ) ↔ (x ∈ y ⋀ ∀yφ)))
3	2	exbidv 1277	. . . . . . . 8 ⊢ (w = y → (∃x(x ∈ w ⋀ ∀yφ) ↔ ∃x(x ∈ y ⋀ ∀yφ)))
4	3	bibi2d 617	. . . . . . 7 ⊢ (w = y → ((z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ (z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
5	4	albidv 1276	. . . . . 6 ⊢ (w = y → (∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
6	5	exbidv 1277	. . . . 5 ⊢ (w = y → (∃x∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ ∃x∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
7	6	imbi2d 611	. . . 4 ⊢ (w = y → ((∀x∃y∀z(φ → z = y) → ∃x∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ))) ↔ (∀x∃y∀z(φ → z = y) → ∃x∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))))
8		ax-4 971	. . . . . . . . . 10 ⊢ (∀yφ → φ)
9	8	imim1i 16	. . . . . . . . 9 ⊢ ((φ → z = y) → (∀yφ → z = y))
10	9	19.20i 990	. . . . . . . 8 ⊢ (∀z(φ → z = y) → ∀z(∀yφ → z = y))
11	10	19.22i 1038	. . . . . . 7 ⊢ (∃y∀z(φ → z = y) → ∃y∀z(∀yφ → z = y))
12	11	19.20i 990	. . . . . 6 ⊢ (∀x∃y∀z(φ → z = y) → ∀x∃y∀z(∀yφ → z = y))
13		ax-rep 2689	. . . . . 6 ⊢ (∀x∃y∀z(∀yφ → z = y) → ∃y∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)))
14	12, 13	syl 10	. . . . 5 ⊢ (∀x∃y∀z(φ → z = y) → ∃y∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)))
15		ax-17 969	. . . . . . . 8 ⊢ (z ∈ y → ∀x z ∈ y)
16		hbe1 1014	. . . . . . . 8 ⊢ (∃x(x ∈ w ⋀ ∀yφ) → ∀x∃x(x ∈ w ⋀ ∀yφ))
17	15, 16	hbbi 1008	. . . . . . 7 ⊢ ((z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)) → ∀x(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)))
18	17	hbal 1003	. . . . . 6 ⊢ (∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)) → ∀x∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)))
19		ax-17 969	. . . . . . . 8 ⊢ (z ∈ x → ∀y z ∈ x)
20		ax-17 969	. . . . . . . . . 10 ⊢ (x ∈ w → ∀y x ∈ w)
21		hba1 1001	. . . . . . . . . 10 ⊢ (∀yφ → ∀y∀yφ)
22	20, 21	hban 1007	. . . . . . . . 9 ⊢ ((x ∈ w ⋀ ∀yφ) → ∀y(x ∈ w ⋀ ∀yφ))
23	22	hbex 1004	. . . . . . . 8 ⊢ (∃x(x ∈ w ⋀ ∀yφ) → ∀y∃x(x ∈ w ⋀ ∀yφ))
24	19, 23	hbbi 1008	. . . . . . 7 ⊢ ((z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) → ∀y(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)))
25	24	hbal 1003	. . . . . 6 ⊢ (∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)) → ∀y∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)))
26		elequ2 1135	. . . . . . . 8 ⊢ (y = x → (z ∈ y ↔ z ∈ x))
27	26	bibi1d 618	. . . . . . 7 ⊢ (y = x → ((z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ (z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ))))
28	27	albidv 1276	. . . . . 6 ⊢ (y = x → (∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ))))
29	18, 25, 28	cbvex 1164	. . . . 5 ⊢ (∃y∀z(z ∈ y ↔ ∃x(x ∈ w ⋀ ∀yφ)) ↔ ∃x∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)))
30	14, 29	sylib 198	. . . 4 ⊢ (∀x∃y∀z(φ → z = y) → ∃x∀z(z ∈ x ↔ ∃x(x ∈ w ⋀ ∀yφ)))
31	7, 30	chvarv 1325	. . 3 ⊢ (∀x∃y∀z(φ → z = y) → ∃x∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))
32	31	19.35ri 1075	. 2 ⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)))
33		ax-17 969	. . . . . . . . 9 ⊢ (φ → ∀yφ)
34	33	19.3 1029	. . . . . . . 8 ⊢ (∀yφ ↔ φ)
35	34	anbi2i 480	. . . . . . 7 ⊢ ((x ∈ y ⋀ ∀yφ) ↔ (x ∈ y ⋀ φ))
36	35	exbii 1049	. . . . . 6 ⊢ (∃x(x ∈ y ⋀ ∀yφ) ↔ ∃x(x ∈ y ⋀ φ))
37	36	bibi2i 607	. . . . 5 ⊢ ((z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)) ↔ (z ∈ x ↔ ∃x(x ∈ y ⋀ φ)))
38	37	albii 997	. . . 4 ⊢ (∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ φ)))
39	38	imbi2i 185	. . 3 ⊢ ((∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) ↔ (∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ φ))))
40	39	exbii 1049	. 2 ⊢ (∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))) ↔ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ φ))))
41	32, 40	mpbi 189	1 ⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ φ)))

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

This theorem is referenced by:  axrep2 2691

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 2689

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

Copyright terms: Public domain