Theorem axrepndlem1 10394

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 5221	. 2 ⊢ ∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
2		nfnae 2432	. . 3 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3		nfnae 2432	. . . . 5 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
4		nfnae 2432	. . . . . 6 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
5		nfs1v 2151	. . . . . . . 8 ⊢ Ⅎ𝑧[𝑤 / 𝑧]𝜑
6	5	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧[𝑤 / 𝑧]𝜑)
7		nfcvd 2906	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑤)
8		nfcvf2 2935	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦)
9	7, 8	nfeqd 2915	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
10	6, 9	nfimd 1895	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦))
11		sbequ12r 2243	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
12		equequ1 2026	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 = 𝑦 ↔ 𝑧 = 𝑦))
13	11, 12	imbi12d 345	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))
14	13	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))))
15	4, 10, 14	cbvald 2405	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦)))
16	3, 15	exbid 2214	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)))
17		nfvd 1916	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 ∈ 𝑥)
18	8	nfcrd 2894	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑥 ∈ 𝑦)
19	3, 6	nfald 2320	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑦[𝑤 / 𝑧]𝜑)
20	18, 19	nfand 1898	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
21	2, 20	nfexd 2321	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))
22	17, 21	nfbid 1903	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)))
23		elequ1 2111	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
24	23	adantl 483	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
25		nfeqf2 2375	. . . . . . . . . . 11 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 = 𝑧)
26	3, 25	nfan1 2191	. . . . . . . . . 10 ⊢ Ⅎ𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧)
27	11	adantl 483	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ([𝑤 / 𝑧]𝜑 ↔ 𝜑))
28	26, 27	albid 2213	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∀𝑦[𝑤 / 𝑧]𝜑 ↔ ∀𝑦𝜑))
29	28	anbi2d 630	. . . . . . . 8 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
30	29	exbidv 1922	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
31	24, 30	bibi12d 346	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
32	31	ex 414	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
33	4, 22, 32	cbvald 2405	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
34	16, 33	imbi12d 345	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ((∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
35	2, 34	exbid 2214	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))
36	1, 35	mpbii 232	1 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1537  ∃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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-13 2370  ax-ext 2707  ax-rep 5218

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-cleq 2728  df-clel 2814  df-nfc 2887

This theorem is referenced by:  axrepndlem2  10395