Theorem zfcndrep 4949

Description: Axiom of Replacement, reproved from conditionless ZFC axioms.

Assertion

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

Distinct variable group:   x,y,z,w

Proof of Theorem zfcndrep

Step	Hyp	Ref	Expression
1		hbe1 1015	. . . . . 6 ⊢ (∃y∀z(∀yφ → z = y) → ∀y∃y∀z(∀yφ → z = y))
2		ax-17 970	. . . . . . . 8 ⊢ (z ∈ w → ∀y z ∈ w)
3		ax-17 970	. . . . . . . . . 10 ⊢ (w ∈ x → ∀y w ∈ x)
4		hba1 1002	. . . . . . . . . 10 ⊢ (∀y∀yφ → ∀y∀y∀yφ)
5	3, 4	hban 1008	. . . . . . . . 9 ⊢ ((w ∈ x ⋀ ∀y∀yφ) → ∀y(w ∈ x ⋀ ∀y∀yφ))
6	5	hbex 1005	. . . . . . . 8 ⊢ (∃w(w ∈ x ⋀ ∀y∀yφ) → ∀y∃w(w ∈ x ⋀ ∀y∀yφ))
7	2, 6	hbbi 1009	. . . . . . 7 ⊢ ((z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)) → ∀y(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))
8	7	hbal 1004	. . . . . 6 ⊢ (∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)) → ∀y∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))
9	1, 8	hbim 1006	. . . . 5 ⊢ ((∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))) → ∀y(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))))
10	9	hbex 1005	. . . 4 ⊢ (∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))) → ∀y∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))))
11		elequ2 1136	. . . . . . . . . 10 ⊢ (y = x → (w ∈ y ↔ w ∈ x))
12	11	anbi1d 616	. . . . . . . . 9 ⊢ (y = x → ((w ∈ y ⋀ ∀y∀yφ) ↔ (w ∈ x ⋀ ∀y∀yφ)))
13	12	exbidv 1278	. . . . . . . 8 ⊢ (y = x → (∃w(w ∈ y ⋀ ∀y∀yφ) ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))
14	13	bibi2d 617	. . . . . . 7 ⊢ (y = x → ((z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ)) ↔ (z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))))
15	14	albidv 1277	. . . . . 6 ⊢ (y = x → (∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ)) ↔ ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ))))
16	15	imbi2d 611	. . . . 5 ⊢ (y = x → ((∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ))) ↔ (∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))))
17	16	exbidv 1278	. . . 4 ⊢ (y = x → (∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ))) ↔ ∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))))
18		axrepnd 4929	. . . . 5 ⊢ ∃w(∃y∀z(∀yφ → z = y) → ∀z(∀y z ∈ w ↔ ∃w(∀z w ∈ y ⋀ ∀y∀yφ)))
19	2	19.3 1030	. . . . . . . . 9 ⊢ (∀y z ∈ w ↔ z ∈ w)
20		ax-17 970	. . . . . . . . . . . 12 ⊢ (w ∈ y → ∀z w ∈ y)
21	20	19.3 1030	. . . . . . . . . . 11 ⊢ (∀z w ∈ y ↔ w ∈ y)
22	21	anbi1i 481	. . . . . . . . . 10 ⊢ ((∀z w ∈ y ⋀ ∀y∀yφ) ↔ (w ∈ y ⋀ ∀y∀yφ))
23	22	exbii 1050	. . . . . . . . 9 ⊢ (∃w(∀z w ∈ y ⋀ ∀y∀yφ) ↔ ∃w(w ∈ y ⋀ ∀y∀yφ))
24	19, 23	bibi12i 609	. . . . . . . 8 ⊢ ((∀y z ∈ w ↔ ∃w(∀z w ∈ y ⋀ ∀y∀yφ)) ↔ (z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ)))
25	24	albii 998	. . . . . . 7 ⊢ (∀z(∀y z ∈ w ↔ ∃w(∀z w ∈ y ⋀ ∀y∀yφ)) ↔ ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ)))
26	25	imbi2i 185	. . . . . 6 ⊢ ((∃y∀z(∀yφ → z = y) → ∀z(∀y z ∈ w ↔ ∃w(∀z w ∈ y ⋀ ∀y∀yφ))) ↔ (∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ))))
27	26	exbii 1050	. . . . 5 ⊢ (∃w(∃y∀z(∀yφ → z = y) → ∀z(∀y z ∈ w ↔ ∃w(∀z w ∈ y ⋀ ∀y∀yφ))) ↔ ∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ))))
28	18, 27	mpbi 189	. . . 4 ⊢ ∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ⋀ ∀y∀yφ)))
29	10, 17, 28	chvar 1166	. . 3 ⊢ ∃w(∃y∀z(∀yφ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))
30	29	19.35i 1075	. 2 ⊢ (∀w∃y∀z(∀yφ → z = y) → ∃w∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)))
31		ax-17 970	. . . . 5 ⊢ (z ∈ y → ∀w z ∈ y)
32		hbe1 1015	. . . . 5 ⊢ (∃w(w ∈ x ⋀ ∀yφ) → ∀w∃w(w ∈ x ⋀ ∀yφ))
33	31, 32	hbbi 1009	. . . 4 ⊢ ((z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)) → ∀w(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)))
34	33	hbal 1004	. . 3 ⊢ (∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)) → ∀w∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)))
35		elequ2 1136	. . . . 5 ⊢ (w = y → (z ∈ w ↔ z ∈ y))
36		hba1 1002	. . . . . . . . 9 ⊢ (∀yφ → ∀y∀yφ)
37	36	19.3 1030	. . . . . . . 8 ⊢ (∀y∀yφ ↔ ∀yφ)
38	37	anbi2i 480	. . . . . . 7 ⊢ ((w ∈ x ⋀ ∀y∀yφ) ↔ (w ∈ x ⋀ ∀yφ))
39	38	exbii 1050	. . . . . 6 ⊢ (∃w(w ∈ x ⋀ ∀y∀yφ) ↔ ∃w(w ∈ x ⋀ ∀yφ))
40	39	a1i 8	. . . . 5 ⊢ (w = y → (∃w(w ∈ x ⋀ ∀y∀yφ) ↔ ∃w(w ∈ x ⋀ ∀yφ)))
41	35, 40	bibi12d 628	. . . 4 ⊢ (w = y → ((z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)) ↔ (z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ))))
42	41	albidv 1277	. . 3 ⊢ (w = y → (∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)) ↔ ∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ))))
43	8, 34, 42	cbvex 1165	. 2 ⊢ (∃w∀z(z ∈ w ↔ ∃w(w ∈ x ⋀ ∀y∀yφ)) ↔ ∃y∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)))
44	30, 43	sylib 198	1 ⊢ (∀w∃y∀z(∀yφ → z = y) → ∃y∀z(z ∈ y ↔ ∃w(w ∈ x ⋀ ∀yφ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-15 1359  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-pow 2738  ax-reg 4576

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410

Copyright terms: Public domain