Theorem axrepnd 4966

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 4965	. . . 4 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
2		hbnae 1151	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
3		hbnae 1151	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
4	2, 3	hban 1013	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
5		hbnae 1151	. . . . . 6 ⊢ (¬ ∀y y = z → ∀x ¬ ∀y y = z)
6	4, 5	hban 1013	. . . . 5 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∀x((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z))
7		hbnae 1151	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
8		hbnae 1151	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
9	7, 8	hban 1013	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ⋀ ¬ ∀x x = z))
10		hbnae 1151	. . . . . . . 8 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
11	9, 10	hban 1013	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∀z((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z))
12		ax-15 1364	. . . . . . . . . . . . 13 ⊢ (¬ ∀y y = z → (¬ ∀y y = x → (z ∈ x → ∀y z ∈ x)))
13	12	com12 11	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = x → (¬ ∀y y = z → (z ∈ x → ∀y z ∈ x)))
14	13	nalequcoms 1148	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (¬ ∀y y = z → (z ∈ x → ∀y z ∈ x)))
15	14	imp 350	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
16	15	adantlr 395	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
17		ax-4 977	. . . . . . . . 9 ⊢ (∀y z ∈ x → z ∈ x)
18	16, 17	impbid1 520	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (z ∈ x ↔ ∀y z ∈ x))
19		ax-15 1364	. . . . . . . . . . . . . 14 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
20	19	imp 350	. . . . . . . . . . . . 13 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → (x ∈ y → ∀z x ∈ y))
21		alequcom 1146	. . . . . . . . . . . . . 14 ⊢ (∀z z = x → ∀x x = z)
22	21	con3i 98	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → ¬ ∀z z = x)
23		alequcom 1146	. . . . . . . . . . . . . 14 ⊢ (∀z z = y → ∀y y = z)
24	23	con3i 98	. . . . . . . . . . . . 13 ⊢ (¬ ∀y y = z → ¬ ∀z z = y)
25	20, 22, 24	syl2an 457	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
26	25	adantll 394	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
27		ax-4 977	. . . . . . . . . . 11 ⊢ (∀z x ∈ y → x ∈ y)
28	26, 27	impbid1 520	. . . . . . . . . 10 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (x ∈ y ↔ ∀z x ∈ y))
29	28	anbi1d 620	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ((x ∈ y ⋀ ∀yφ) ↔ (∀z x ∈ y ⋀ ∀yφ)))
30	6, 29	exbid 1109	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (∃x(x ∈ y ⋀ ∀yφ) ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
31	18, 30	bibi12d 632	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ((z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ)) ↔ (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
32	11, 31	albid 1108	. . . . . 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φ))))
33	32	imbi2d 615	. . . . 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φ)))))
34	6, 33	exbid 1109	. . . 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φ)))))
35	1, 34	mpbid 195	. . 3 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
36	35	exp31 378	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ ∀y y = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))))
37		hbae 1149	. . . . 5 ⊢ (∀x x = y → ∀z∀x x = y)
38		pm5.21 681	. . . . . 6 ⊢ ((¬ ∀y z ∈ x ⋀ ¬ ∃x(∀z x ∈ y ⋀ ∀yφ)) → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
39		nd2 4959	. . . . . . 7 ⊢ (∀y y = x → ¬ ∀y z ∈ x)
40	39	alequcoms 1147	. . . . . 6 ⊢ (∀x x = y → ¬ ∀y z ∈ x)
41		hbae 1149	. . . . . . 7 ⊢ (∀x x = y → ∀x∀x x = y)
42		nd3 4960	. . . . . . . 8 ⊢ (∀x x = y → ¬ ∀z x ∈ y)
43	42	intnanrd 698	. . . . . . 7 ⊢ (∀x x = y → ¬ (∀z x ∈ y ⋀ ∀yφ))
44	41, 43	nexd 1106	. . . . . 6 ⊢ (∀x x = y → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
45	38, 40, 44	sylanc 474	. . . . 5 ⊢ (∀x x = y → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
46	37, 45	19.21ai 1002	. . . 4 ⊢ (∀x x = y → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
47	46	a1d 12	. . 3 ⊢ (∀x x = y → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
48		19.8a 1033	. . 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φ))))
49	47, 48	syl 10	. 2 ⊢ (∀x x = y → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
50		hbae 1149	. . . . 5 ⊢ (∀x x = z → ∀z∀x x = z)
51		nd4 4961	. . . . . 6 ⊢ (∀x x = z → ¬ ∀y z ∈ x)
52		hbae 1149	. . . . . . 7 ⊢ (∀x x = z → ∀x∀x x = z)
53		nd1 4958	. . . . . . . . 9 ⊢ (∀z z = x → ¬ ∀z x ∈ y)
54	53	alequcoms 1147	. . . . . . . 8 ⊢ (∀x x = z → ¬ ∀z x ∈ y)
55	54	intnanrd 698	. . . . . . 7 ⊢ (∀x x = z → ¬ (∀z x ∈ y ⋀ ∀yφ))
56	52, 55	nexd 1106	. . . . . 6 ⊢ (∀x x = z → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
57	38, 51, 56	sylanc 474	. . . . 5 ⊢ (∀x x = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
58	50, 57	19.21ai 1002	. . . 4 ⊢ (∀x x = z → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
59	58	a1d 12	. . 3 ⊢ (∀x x = z → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
60	59, 48	syl 10	. 2 ⊢ (∀x x = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
61		hbae 1149	. . . . 5 ⊢ (∀y y = z → ∀z∀y y = z)
62		nd1 4958	. . . . . 6 ⊢ (∀y y = z → ¬ ∀y z ∈ x)
63		hbae 1149	. . . . . . 7 ⊢ (∀y y = z → ∀x∀y y = z)
64		nd2 4959	. . . . . . . . 9 ⊢ (∀z z = y → ¬ ∀z x ∈ y)
65	64	alequcoms 1147	. . . . . . . 8 ⊢ (∀y y = z → ¬ ∀z x ∈ y)
66	65	intnanrd 698	. . . . . . 7 ⊢ (∀y y = z → ¬ (∀z x ∈ y ⋀ ∀yφ))
67	63, 66	nexd 1106	. . . . . 6 ⊢ (∀y y = z → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
68	38, 62, 67	sylanc 474	. . . . 5 ⊢ (∀y y = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
69	61, 68	19.21ai 1002	. . . 4 ⊢ (∀y y = z → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
70	69	a1d 12	. . 3 ⊢ (∀y y = z → (∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
71	70, 48	syl 10	. 2 ⊢ (∀y y = z → ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ))))
72	36, 49, 60, 71	pm2.61iii 132	1 ⊢ ∃x(∃y∀z(φ → z = y) → ∀z(∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 958   = wceq 960   ∈ wcel 962  ∃wex 984

This theorem is referenced by:  zfcndrep 4986

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-15 1364  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-pow 2758  ax-reg 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425

Copyright terms: Public domain