Theorem axrepndlem1 10658

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.) (New usage is discouraged.)

Assertion

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

Distinct variable groups:   𝑥,𝑧   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧)

Proof of Theorem axrepndlem1

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axrep2 5235	. 2 ⊢ ∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
2		nfnae 2464	. . 3 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3		nfnae 2464	. . . . 5 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
4		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
5		nfs1v 2193	. . . . . . . 8 ⊢ Ⅎ𝑧[𝑤 / 𝑧]𝜑
6	5	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧[𝑤 / 𝑧]𝜑)
7		nfcvd 2924	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑤)
8		nfcvf2 2950	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦)
9	7, 8	nfeqd 2933	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
10	6, 9	nfimd 1927	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦))
11		sbequ12r 2288	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
12		equequ1 2058	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 = 𝑦 ↔ 𝑧 = 𝑦))
13	11, 12	imbi12d 347	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))
14	13	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))))
15	4, 10, 14	cbvald 2437	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦)))
16	3, 15	exbid 2260	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)))
17		nfvd 1948	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 ∈ 𝑥)
18	8	nfcrd 2917	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑥 ∈ 𝑦)
19	3, 6	nfald 2359	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑦[𝑤 / 𝑧]𝜑)
20	18, 19	nfand 1930	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
21	2, 20	nfexd 2360	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
22	17, 21	nfbid 1935	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
23		elequ1 2152	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
24	23	adantl 487	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
25		nfeqf2 2407	. . . . . . . . . . 11 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 = 𝑧)
26	3, 25	nfan1 2237	. . . . . . . . . 10 ⊢ Ⅎ𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧)
27	11	adantl 487	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
28	26, 27	albid 2259	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∀𝑦[𝑤 / 𝑧]𝜑 ↔ ∀𝑦𝜑))
29	28	anbi2d 642	. . . . . . . 8 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
30	29	exbidv 1954	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
31	24, 30	bibi12d 348	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
32	31	ex 418	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
33	4, 22, 32	cbvald 2437	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
34	16, 33	imbi12d 347	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ((∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
35	2, 34	exbid 2260	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
36	1, 35	mpbii 236	1 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))

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

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:  axrepndlem2  10659