Theorem axrepnd 3740

Description: A version of the Axiom of Replacement with no distinct variable conditions.

Assertion

Ref	Expression
axrepnd	⊢ ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))

Proof of Theorem axrepnd

Step	Hyp	Ref	Expression
1		axrepndlem2 3739	. . . 4 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
2		eq6 826	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
3		eq6 826	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
4	2, 3	hban 704	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ∧ ¬ ∀x x = z))
5		eq6 826	. . . . . 6 ⊢ (¬ ∀y y = z → ∀x ¬ ∀y y = z)
6	4, 5	hban 704	. . . . 5 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∀x((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z))
7		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
8		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
9	7, 8	hban 704	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ∧ ¬ ∀x x = z))
10		eq6 826	. . . . . . . 8 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
11	9, 10	hban 704	. . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∀z((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z))
12		ax15 1006	. . . . . . . . . . . . 13 ⊢ (¬ ∀y y = z → (¬ ∀y y = x → (z ∈ x → ∀y z ∈ x)))
13	12	com12 13	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = x → (¬ ∀y y = z → (z ∈ x → ∀y z ∈ x)))
14	13	eq4ds 823	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (¬ ∀y y = z → (z ∈ x → ∀y z ∈ x)))
15	14	imp 277	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
16	15	adantlr 310	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
17		ax-4 673	. . . . . . . . . 10 ⊢ (∀y z ∈ x → z ∈ x)
18	17	a1i 7	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (∀y z ∈ x → z ∈ x))
19	16, 18	impbid 397	. . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (z ∈ x ↔ ∀y z ∈ x))
20		ax15 1006	. . . . . . . . . . . . . 14 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
21	20	imp 277	. . . . . . . . . . . . 13 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → (x ∈ y → ∀z x ∈ y))
22		eq4 821	. . . . . . . . . . . . . 14 ⊢ (∀z z = x → ∀x x = z)
23	22	con3i 90	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → ¬ ∀z z = x)
24		eq4 821	. . . . . . . . . . . . . 14 ⊢ (∀z z = y → ∀y y = z)
25	24	con3i 90	. . . . . . . . . . . . 13 ⊢ (¬ ∀y y = z → ¬ ∀z z = y)
26	21, 23, 25	syl2an 349	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ∧ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
27	26	adantll 309	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
28		ax-4 673	. . . . . . . . . . . 12 ⊢ (∀z x ∈ y → x ∈ y)
29	28	a1i 7	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (∀z x ∈ y → x ∈ y))
30	27, 29	impbid 397	. . . . . . . . . 10 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (x ∈ y ↔ ∀z x ∈ y))
31	30	anbi1d 469	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ((x ∈ y ∧ ∀yφ) ↔ (∀z x ∈ y ∧ ∀yφ)))
32	6, 31	biexd 783	. . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (∃x(x ∈ y ∧ ∀yφ) ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
33	19, 32	bibi12d 477	. . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ((z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)) ↔ (∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
34	11, 33	biald 782	. . . . . 6 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)) ↔ ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
35	34	imbi2d 464	. . . . 5 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ((∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))) ↔ (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))))
36	6, 35	biexd 783	. . . 4 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → (∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))) ↔ ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))))
37	1, 36	mpbid 170	. . 3 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
38	37	exp31 293	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ ∀y y = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))))
39		eq5 824	. . . . 5 ⊢ (∀x x = y → ∀z∀x x = y)
40		pm5.21 502	. . . . . 6 ⊢ ((¬ ∀y z ∈ x ∧ ¬ ∃x(∀z x ∈ y ∧ ∀yφ)) → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
41		nd2 3733	. . . . . . 7 ⊢ (∀y y = x → ¬ ∀y z ∈ x)
42	41	eq4s 822	. . . . . 6 ⊢ (∀x x = y → ¬ ∀y z ∈ x)
43		eq5 824	. . . . . . 7 ⊢ (∀x x = y → ∀x∀x x = y)
44		nd3 3734	. . . . . . . 8 ⊢ (∀x x = y → ¬ ∀z x ∈ y)
45		pm3.26 256	. . . . . . . 8 ⊢ ((∀z x ∈ y ∧ ∀yφ) → ∀z x ∈ y)
46	44, 45	ºsyl 102	. . . . . . 7 ⊢ (∀x x = y → ¬ (∀z x ∈ y ∧ ∀yφ))
47	43, 46	nexd 780	. . . . . 6 ⊢ (∀x x = y → ¬ ∃x(∀z x ∈ y ∧ ∀yφ))
48	40, 42, 47	sylanc 361	. . . . 5 ⊢ (∀x x = y → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
49	39, 48	19.21ai 740	. . . 4 ⊢ (∀x x = y → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
50	49	a1d 14	. . 3 ⊢ (∀x x = y → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
51		19.8a 712	. . 3 ⊢ ((∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))) → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
52	50, 51	syl 12	. 2 ⊢ (∀x x = y → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
53		eq5 824	. . . . 5 ⊢ (∀x x = z → ∀z∀x x = z)
54		nd4 3735	. . . . . 6 ⊢ (∀x x = z → ¬ ∀y z ∈ x)
55		eq5 824	. . . . . . 7 ⊢ (∀x x = z → ∀x∀x x = z)
56	&nbs<;	nd1 3732	. . . . . . . . 9 ⊢ (∀z z/I> = x → ¬ ∀z x ∈ y)
57	56	eq4s 822	. . . . . . . 8 ⊢ (∀x x = z → ¬ ∀z x ∈ y)
58	57, 45	nsyl 102	. . . . . . 7 ⊢ (∀x x = z → ¬ (∀z x ∈ y ∧ ∀yφ))
59	55, 58	nexd 780	. . . . . 6 ⊢ (∀x x = z → ¬ ∃x(∀z x ∈ y ∧ ∀yφ))
60	40, 54, 59	sylanc 361	. . . . 5 ⊢ (∀x x = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
61	53, 60	19.21ai 740	. . . 4 ⊢ (∀x x = z → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
62	61	a1d 14	. . 3 ⊢ (∀x x = z → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
63	62, 51	syl 12	. 2 ⊢ (∀x x = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
64		eq5 824	. . . . 5 ⊢ (∀y y = z → ∀z∀y y = z)
65		nd1 3732	. . . . . 6 ⊢ (∀y y = z → ¬ ∀y z ∈ x)
66		eq5 824	. . . . . . 7 ⊢ (∀y y = z → ∀x∀y y = z)
67		nd2 3733	. . . . . . . . 9 ⊢ (∀z z = y → ¬ ∀z x ∈ y)
68	67	eq4s 822	. . . . . . . 8 ⊢ (∀y y = z → ¬ ∀z x ∈ y)
69	68, 45	nsyl 102	. . . . . . 7 ⊢ (∀y y = z → ¬ (∀z x ∈ y ∧ ∀yφ))
70	66, 69	nexd 780	. . . . . 6 ⊢ (∀y y = z → ¬ ∃x(∀z x ∈ y ∧ ∀yφ))
71	40, 65, 70	sylanc 361	. . . . 5 ⊢ (∀y y = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
72	64, 71	19.21ai 740	. . . 4 ⊢ (∀y y = z → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))
73	72	a1d 14	. . 3 ⊢ (∀y y = z → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
74	73, 51	syl 12	. 2 ⊢ (∀y y = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ))))
75	38, 52, 63, 74	pm2.61iii 114	1 ⊢ ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ∧ ∀yφ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803

This theorem is referenced by:  zfcndrep 3760

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077  ax-reg 1078

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812

metamath.org