Theorem axrepndlem2 10659

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (New usage is discouraged.)

Assertion

Ref	Expression
axrepndlem2	⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))

Proof of Theorem axrepndlem2

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axrepndlem1 10658	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑤(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
2		nfnae 2464	. . . . 5 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
3		nfnae 2464	. . . . 5 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
4	2, 3	nfan 1932	. . . 4 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
5		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
6		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
7	5, 6	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
8		nfnae 2464	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
9		nfnae 2464	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
10	8, 9	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
11		nfs1v 2193	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
12	11	a1i 11	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥[𝑤 / 𝑥]𝜑)
13		nfcvf 2949	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧)
14	13	adantl 487	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧)
15		nfcvf 2949	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
16	15	adantr 486	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦)
17	14, 16	nfeqd 2933	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 = 𝑦)
18	12, 17	nfimd 1927	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦))
19	10, 18	nfald 2359	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦))
20	7, 19	nfexd 2360	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦))
21		nfcvd 2924	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤)
22	14, 21	nfeld 2934	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 ∈ 𝑤)
23		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑤(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
24	21, 16	nfeld 2934	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑦)
25	7, 12	nfald 2359	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦[𝑤 / 𝑥]𝜑)
26	24, 25	nfand 1930	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
27	23, 26	nfexd 2360	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))
28	22, 27	nfbid 1935	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
29	10, 28	nfald 2359	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))
30	20, 29	nfimd 1927	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))))
31		nfcvd 2924	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤)
32		nfcvf2 2950	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
33	32	adantr 486	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥)
34	31, 33	nfeqd 2933	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥)
35	7, 34	nfan1 2237	. . . . . . 7 ⊢ Ⅎ𝑦((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
36		nfcvd 2924	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑤)
37		nfcvf2 2950	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥)
38	37	adantl 487	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑥)
39	36, 38	nfeqd 2933	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥)
40	10, 39	nfan1 2237	. . . . . . . 8 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
41		sbequ12r 2288	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
42	41	imbi1d 344	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))
43	42	adantl 487	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))
44	40, 43	albid 2259	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦)))
45	35, 44	exbid 2260	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)))
46		elequ2 2160	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥))
47	46	adantl 487	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥))
48		elequ1 2152	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
49	48	adantl 487	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
50	41	adantl 487	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
51	35, 50	albid 2259	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦[𝑤 / 𝑥]𝜑 ↔ ∀𝑦𝜑))
52	49, 51	anbi12d 644	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
53	52	ex 418	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
54	4, 26, 53	cbvexd 2438	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
55	54	adantr 486	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
56	47, 55	bibi12d 348	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
57	40, 56	albid 2259	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
58	45, 57	imbi12d 347	. . . . 5 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
59	58	ex 418	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))))
60	4, 30, 59	cbvexd 2438	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
61	1, 60	imbitrid 247	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
62	61	imp 412	1 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816  [wsb 2099  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2402  ax-ext 2733  ax-rep 5232

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is used by:  axrepnd  10660