Theorem mh-setindnd

Description: A version of mh-setind with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	mh-setindnd	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑦 𝜑 → 𝜑 )
2	1	imim2i	⊢ ( ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ( 𝑥 ∈ 𝑦 → 𝜑 ) )
3	2	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) )
4	3	imim1i	⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) )
5	4	alimi	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) )
6		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
7		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑦 ) )
8	6 7	mtbii	⊢ ( 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝑦 )
9	8	pm2.21d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) )
10	9	alimi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) )
11		sp	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
12	1	a1i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → 𝜑 ) )
13	11 12	embantd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) → 𝜑 ) )
14	13	spsd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) → 𝜑 ) )
15	10 14	embantd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 ) )
16	15	spsd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 ) )
17		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
18		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
19		dveel1	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝑥 ∈ 𝑧 ) )
20	19	naecoms	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝑥 ∈ 𝑧 ) )
21	17 20	nf5d	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ∈ 𝑧 )
22		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
23	22	a1i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∀ 𝑦 𝜑 )
24	21 23	nfimd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) )
25	18 24	nfald	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) )
26		nfeqf1	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 = 𝑧 )
27	26	naecoms	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑧 )
28	27 23	nfimd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) )
29	18 28	nfald	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) )
30	25 29	nfimd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) )
31		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 )
32	18 31	nfan1	⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 )
33		elequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦 ) )
34	33	imbi1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) ) )
35	34	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) ) )
36	32 35	albid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) ) )
37		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
38	37	imbi1d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) )
39	38	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) )
40	32 39	albid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) )
41	36 40	imbi12d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦 ) → ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) ) )
42	41	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) ) ) )
43	17 30 42	cbvaldw	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) ) )
44		mh-setind	⊢ ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) → ∀ 𝑦 𝜑 )
45	44	19.21bi	⊢ ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ) → 𝜑 )
46	43 45	biimtrrdi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 ) )
47	16 46	pm2.61i	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 )
48	5 47	syl	⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑦 𝜑 ) ) → 𝜑 )