Metamath Proof Explorer

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 ⊢ ∀ y ∀ x x ∈ y → φ → ∀ x x = y → ∀ y φ → φ

Proof

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