Theorem axrepndlem1 10611

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2377. (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 5257	. 2 ⊢ ∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
2		nfnae 2439	. . 3 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3		nfnae 2439	. . . . 5 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
4		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
5		nfs1v 2157	. . . . . . . 8 ⊢ Ⅎ𝑧[𝑤 / 𝑧]𝜑
6	5	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧[𝑤 / 𝑧]𝜑)
7		nfcvd 2900	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑤)
8		nfcvf2 2927	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦)
9	7, 8	nfeqd 2910	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
10	6, 9	nfimd 1894	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦))
11		sbequ12r 2253	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
12		equequ1 2025	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 = 𝑦 ↔ 𝑧 = 𝑦))
13	11, 12	imbi12d 344	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))
14	13	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))))
15	4, 10, 14	cbvald 2412	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦)))
16	3, 15	exbid 2224	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)))
17		nfvd 1915	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 ∈ 𝑥)
18	8	nfcrd 2893	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑥 ∈ 𝑦)
19	3, 6	nfald 2329	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑦[𝑤 / 𝑧]𝜑)
20	18, 19	nfand 1897	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
21	2, 20	nfexd 2330	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
22	17, 21	nfbid 1902	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
23		elequ1 2116	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
24	23	adantl 481	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
25		nfeqf2 2382	. . . . . . . . . . 11 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 = 𝑧)
26	3, 25	nfan1 2201	. . . . . . . . . 10 ⊢ Ⅎ𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧)
27	11	adantl 481	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
28	26, 27	albid 2223	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∀𝑦[𝑤 / 𝑧]𝜑 ↔ ∀𝑦𝜑))
29	28	anbi2d 630	. . . . . . . 8 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
30	29	exbidv 1921	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
31	24, 30	bibi12d 345	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
32	31	ex 412	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
33	4, 22, 32	cbvald 2412	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
34	16, 33	imbi12d 344	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ((∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
35	2, 34	exbid 2224	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
36	1, 35	mpbii 233	1 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2377  ax-ext 2708  ax-rep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-cleq 2728  df-clel 2810  df-nfc 2886

This theorem is referenced by:  axrepndlem2  10612