Theorem axrepnd 4926

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 4925	. . . 4 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ⋀ ∀yφ))))
2		hbnae 1145	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
3		hbnae 1145	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
4	2, 3	hban 1007	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
5		hbnae 1145	. . . . . 6 ⊢ (¬ ∀y y = z → ∀x ¬ ∀y y = z)
6	4, 5	hban 1007	. . . . 5 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∀x((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z))
7		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
8		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
9	7, 8	hban 1007	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ⋀ ¬ ∀x x = z))
10		hbnae 1145	. . . . . . . 8 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
11	9, 10	hban 1007	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ∀z((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z))
12		ax-15 1358	. . . . . . . . . . . . 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 1142	. . . . . . . . . . 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 393	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
17		ax-4 971	. . . . . . . . 9 ⊢ (∀y z ∈ x → z ∈ x)
18	16, 17	impbid1 516	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (z ∈ x ↔ ∀y z ∈ x))
19		ax-15 1358	. . . . . . . . . . . . . 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 1140	. . . . . . . . . . . . . 14 ⊢ (∀z z = x → ∀x x = z)
22	21	con3i 98	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → ¬ ∀z z = x)
23		alequcom 1140	. . . . . . . . . . . . . 14 ⊢ (∀z z = y → ∀y y = z)
24	23	con3i 98	. . . . . . . . . . . . 13 ⊢ (¬ ∀y y = z → ¬ ∀z z = y)
25	20, 22, 24	syl2an 454	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
26	25	adantll 392	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (x ∈ y → ∀z x ∈ y))
27		ax-4 971	. . . . . . . . . . 11 ⊢ (∀z x ∈ y → x ∈ y)
28	26, 27	impbid1 516	. . . . . . . . . 10 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (x ∈ y ↔ ∀z x ∈ y))
29	28	anbi1d 616	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → ((x ∈ y ⋀ ∀yφ) ↔ (∀z x ∈ y ⋀ ∀yφ)))
30	6, 29	exbid 1103	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ¬ ∀y y = z) → (∃x(x ∈ y ⋀ ∀yφ) ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
31	18, 30	bibi12d 628	. . . . . . 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 1102	. . . . . 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 611	. . . . 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 1103	. . . 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 376	. 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 1143	. . . . 5 ⊢ (∀x x = y → ∀z∀x x = y)
38		pm5.21 676	. . . . . 6 ⊢ ((¬ ∀y z ∈ x ⋀ ¬ ∃x(∀z x ∈ y ⋀ ∀yφ)) → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
39		nd2 4919	. . . . . . 7 ⊢ (∀y y = x → ¬ ∀y z ∈ x)
40	39	alequcoms 1141	. . . . . 6 ⊢ (∀x x = y → ¬ ∀y z ∈ x)
41		hbae 1143	. . . . . . 7 ⊢ (∀x x = y → ∀x∀x x = y)
42		nd3 4920	. . . . . . . 8 ⊢ (∀x x = y → ¬ ∀z x ∈ y)
43	42	intnanrd 693	. . . . . . 7 ⊢ (∀x x = y → ¬ (∀z x ∈ y ⋀ ∀yφ))
44	41, 43	nexd 1100	. . . . . 6 ⊢ (∀x x = y → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
45	38, 40, 44	sylanc 471	. . . . 5 ⊢ (∀x x = y → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
46	37, 45	19.21ai 996	. . . 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 1027	. . 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 1143	. . . . 5 ⊢ (∀x x = z → ∀z∀x x = z)
51		nd4 4921	. . . . . 6 ⊢ (∀x x = z → ¬ ∀y z ∈ x)
52		hbae 1143	. . . . . . 7 ⊢ (∀x x = z → ∀x∀x x = z)
53		nd1 4918	. . . . . . . . 9 ⊢ (∀z z = x → ¬ ∀z x ∈ y)
54	53	alequcoms 1141	. . . . . . . 8 ⊢ (∀x x = z → ¬ ∀z x ∈ y)
55	54	intnanrd 693	. . . . . . 7 ⊢ (∀x x = z → ¬ (∀z x ∈ y ⋀ ∀yφ))
56	52, 55	nexd 1100	. . . . . 6 ⊢ (∀x x = z → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
57	38, 51, 56	sylanc 471	. . . . 5 ⊢ (∀x x = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
58	50, 57	19.21ai 996	. . . 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 1143	. . . . 5 ⊢ (∀y y = z → ∀z∀y y = z)
62		nd1 4918	. . . . . 6 ⊢ (∀y y = z → ¬ ∀y z ∈ x)
63		hbae 1143	. . . . . . 7 ⊢ (∀y y = z → ∀x∀y y = z)
64		nd2 4919	. . . . . . . . 9 ⊢ (∀z z = y → ¬ ∀z x ∈ y)
65	64	alequcoms 1141	. . . . . . . 8 ⊢ (∀y y = z → ¬ ∀z x ∈ y)
66	65	intnanrd 693	. . . . . . 7 ⊢ (∀y y = z → ¬ (∀z x ∈ y ⋀ ∀yφ))
67	63, 66	nexd 1100	. . . . . 6 ⊢ (∀y y = z → ¬ ∃x(∀z x ∈ y ⋀ ∀yφ))
68	38, 62, 67	sylanc 471	. . . . 5 ⊢ (∀y y = z → (∀y z ∈ x ↔ ∃x(∀z x ∈ y ⋀ ∀yφ)))
69	61, 68	19.21ai 996	. . . 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 952   = wceq 954   ∈ wcel 956  ∃wex 978

This theorem is referenced by:  zfcndrep 4946

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-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-15 1358  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-pow 2737  ax-reg 4573

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409

Copyright terms: Public domain