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	|- ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> A. y ph ) ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		sp	|- ( A. y ph -> ph )
2	1	imim2i	|- ( ( x e. y -> A. y ph ) -> ( x e. y -> ph ) )
3	2	alimi	|- ( A. x ( x e. y -> A. y ph ) -> A. x ( x e. y -> ph ) )
4	3	imim1i	|- ( ( A. x ( x e. y -> ph ) -> A. x ( x = y -> A. y ph ) ) -> ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) )
5	4	alimi	|- ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> A. y ph ) ) -> A. y ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) )
6		elirrv	|- -. x e. x
7		elequ2	|- ( x = y -> ( x e. x <-> x e. y ) )
8	6 7	mtbii	|- ( x = y -> -. x e. y )
9	8	pm2.21d	|- ( x = y -> ( x e. y -> A. y ph ) )
10	9	alimi	|- ( A. x x = y -> A. x ( x e. y -> A. y ph ) )
11		sp	|- ( A. x x = y -> x = y )
12	1	a1i	|- ( A. x x = y -> ( A. y ph -> ph ) )
13	11 12	embantd	|- ( A. x x = y -> ( ( x = y -> A. y ph ) -> ph ) )
14	13	spsd	|- ( A. x x = y -> ( A. x ( x = y -> A. y ph ) -> ph ) )
15	10 14	embantd	|- ( A. x x = y -> ( ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) -> ph ) )
16	15	spsd	|- ( A. x x = y -> ( A. y ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) -> ph ) )
17		nfnae	|- F/ y -. A. x x = y
18		nfnae	|- F/ x -. A. x x = y
19		dveel1	|- ( -. A. y y = x -> ( x e. z -> A. y x e. z ) )
20	19	naecoms	|- ( -. A. x x = y -> ( x e. z -> A. y x e. z ) )
21	17 20	nf5d	|- ( -. A. x x = y -> F/ y x e. z )
22		nfa1	|- F/ y A. y ph
23	22	a1i	|- ( -. A. x x = y -> F/ y A. y ph )
24	21 23	nfimd	|- ( -. A. x x = y -> F/ y ( x e. z -> A. y ph ) )
25	18 24	nfald	|- ( -. A. x x = y -> F/ y A. x ( x e. z -> A. y ph ) )
26		nfeqf1	|- ( -. A. y y = x -> F/ y x = z )
27	26	naecoms	|- ( -. A. x x = y -> F/ y x = z )
28	27 23	nfimd	|- ( -. A. x x = y -> F/ y ( x = z -> A. y ph ) )
29	18 28	nfald	|- ( -. A. x x = y -> F/ y A. x ( x = z -> A. y ph ) )
30	25 29	nfimd	|- ( -. A. x x = y -> F/ y ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) )
31		nfeqf2	|- ( -. A. x x = y -> F/ x z = y )
32	18 31	nfan1	|- F/ x ( -. A. x x = y /\ z = y )
33		elequ2	|- ( z = y -> ( x e. z <-> x e. y ) )
34	33	imbi1d	|- ( z = y -> ( ( x e. z -> A. y ph ) <-> ( x e. y -> A. y ph ) ) )
35	34	adantl	|- ( ( -. A. x x = y /\ z = y ) -> ( ( x e. z -> A. y ph ) <-> ( x e. y -> A. y ph ) ) )
36	32 35	albid	|- ( ( -. A. x x = y /\ z = y ) -> ( A. x ( x e. z -> A. y ph ) <-> A. x ( x e. y -> A. y ph ) ) )
37		equequ2	|- ( z = y -> ( x = z <-> x = y ) )
38	37	imbi1d	|- ( z = y -> ( ( x = z -> A. y ph ) <-> ( x = y -> A. y ph ) ) )
39	38	adantl	|- ( ( -. A. x x = y /\ z = y ) -> ( ( x = z -> A. y ph ) <-> ( x = y -> A. y ph ) ) )
40	32 39	albid	|- ( ( -. A. x x = y /\ z = y ) -> ( A. x ( x = z -> A. y ph ) <-> A. x ( x = y -> A. y ph ) ) )
41	36 40	imbi12d	|- ( ( -. A. x x = y /\ z = y ) -> ( ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) <-> ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) ) )
42	41	ex	|- ( -. A. x x = y -> ( z = y -> ( ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) <-> ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) ) ) )
43	17 30 42	cbvaldw	|- ( -. A. x x = y -> ( A. z ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) <-> A. y ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) ) )
44		mh-setind	|- ( A. z ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) -> A. y ph )
45	44	19.21bi	|- ( A. z ( A. x ( x e. z -> A. y ph ) -> A. x ( x = z -> A. y ph ) ) -> ph )
46	43 45	biimtrrdi	|- ( -. A. x x = y -> ( A. y ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) -> ph ) )
47	16 46	pm2.61i	|- ( A. y ( A. x ( x e. y -> A. y ph ) -> A. x ( x = y -> A. y ph ) ) -> ph )
48	5 47	syl	|- ( A. y ( A. x ( x e. y -> ph ) -> A. x ( x = y -> A. y ph ) ) -> ph )