Step | Hyp | Ref
| Expression |
1 | | 19.26 1878 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤)) |
2 | | elequ1 2117 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
3 | | elequ2 2125 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
4 | 2, 3 | bitrd 282 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
5 | 4 | adantl 485 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
6 | | ax-5 1918 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝑣 → ∀𝑥 𝑣 ∈ 𝑣) |
7 | | ax-5 1918 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑦 → ∀𝑣 𝑦 ∈ 𝑦) |
8 | | elequ1 2117 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣)) |
9 | | elequ2 2125 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑦 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦)) |
10 | 8, 9 | bitrd 282 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦)) |
11 | 6, 7, 10 | dvelimf-o 36680 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥 𝑦 ∈ 𝑦)) |
12 | 4 | biimprcd 253 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) |
13 | 12 | alimi 1819 |
. . . . . . . . 9
⊢
(∀𝑥 𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) |
14 | 11, 13 | syl6 35 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))) |
16 | 5, 15 | sylbid 243 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))) |
17 | 16 | adantl 485 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))) |
18 | | elequ1 2117 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
19 | | elequ2 2125 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) |
20 | 18, 19 | sylan9bb 513 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) |
21 | 20 | sps-o 36659 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) |
22 | | nfa1-o 36666 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) |
23 | 21 | imbi2d 344 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
24 | 22, 23 | albid 2220 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
25 | 21, 24 | imbi12d 348 |
. . . . . 6
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
26 | 25 | adantr 484 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
27 | 17, 26 | mpbid 235 |
. . . 4
⊢
((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
28 | 27 | exp32 424 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
29 | 1, 28 | sylbir 238 |
. 2
⊢
((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
30 | | elequ1 2117 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤)) |
31 | 30 | ad2antll 729 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤)) |
32 | | ax-c14 36642 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))) |
33 | 32 | impcom 411 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)) |
34 | 33 | adantrr 717 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)) |
35 | 30 | biimprcd 253 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑤 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) |
36 | 35 | alimi 1819 |
. . . . . . 7
⊢
(∀𝑥 𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) |
37 | 34, 36 | syl6 35 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))) |
38 | 31, 37 | sylbid 243 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))) |
39 | 38 | adantll 714 |
. . . 4
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))) |
40 | | elequ1 2117 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤)) |
41 | 40 | sps-o 36659 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤)) |
42 | 41 | imbi2d 344 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
43 | 42 | dral2-o 36681 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
44 | 41, 43 | imbi12d 348 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
45 | 44 | ad2antrr 726 |
. . . 4
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
46 | 39, 45 | mpbid 235 |
. . 3
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
47 | 46 | exp32 424 |
. 2
⊢
((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
48 | | elequ2 2125 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
49 | 48 | ad2antll 729 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
50 | | ax-c14 36642 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))) |
51 | 50 | imp 410 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) |
52 | 51 | adantrr 717 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) |
53 | 48 | biimprcd 253 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) |
54 | 53 | alimi 1819 |
. . . . . . 7
⊢
(∀𝑥 𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) |
55 | 52, 54 | syl6 35 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))) |
56 | 49, 55 | sylbid 243 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))) |
57 | 56 | adantlr 715 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))) |
58 | 19 | sps-o 36659 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) |
59 | 58 | imbi2d 344 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
60 | 59 | dral2-o 36681 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
61 | 58, 60 | imbi12d 348 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑤 → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
62 | 61 | ad2antlr 727 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
63 | 57, 62 | mpbid 235 |
. . 3
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
64 | 63 | exp32 424 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
65 | | ax6ev 1978 |
. . . . 5
⊢
∃𝑢 𝑢 = 𝑤 |
66 | | ax6ev 1978 |
. . . . . . 7
⊢
∃𝑣 𝑣 = 𝑧 |
67 | | ax-1 6 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑢 → (𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) |
68 | 67 | alrimiv 1935 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) |
69 | | elequ1 2117 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢)) |
70 | | elequ2 2125 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤)) |
71 | 69, 70 | sylan9bb 513 |
. . . . . . . . . . . 12
⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤)) |
72 | 71 | adantl 485 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤)) |
73 | | dveeq2-o 36684 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧)) |
74 | | dveeq2-o 36684 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤)) |
75 | 73, 74 | im2anan9 623 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))) |
76 | 75 | imp 410 |
. . . . . . . . . . . . 13
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)) |
77 | | 19.26 1878 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)) |
78 | 76, 77 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) |
79 | | nfa1-o 36666 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) |
80 | 71 | sps-o 36659 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤)) |
81 | 80 | imbi2d 344 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
82 | 79, 81 | albid 2220 |
. . . . . . . . . . . 12
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
83 | 78, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
84 | 72, 83 | imbi12d 348 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
85 | 68, 84 | mpbii 236 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
86 | 85 | exp32 424 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
87 | 86 | exlimdv 1941 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
88 | 66, 87 | mpi 20 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
89 | 88 | exlimdv 1941 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
90 | 65, 89 | mpi 20 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))) |
91 | 90 | a1d 25 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |
92 | 91 | a1d 25 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))) |
93 | 29, 47, 64, 92 | 4cases 1041 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) |