Step | Hyp | Ref
| Expression |
1 | | rabn0m 3239 |
. . 3
⊢ (∃z z ∈ {x ∈ A ∣ φ}
↔ ∃x ∈ A φ) |
2 | | df-rab 2309 |
. . . . 5
⊢ {x ∈ A ∣ φ}
= {x ∣ (x ∈ A ∧ φ)} |
3 | 2 | eleq2i 2101 |
. . . 4
⊢ (z ∈ {x ∈ A ∣ φ}
↔ z ∈ {x ∣
(x ∈
A ∧ φ)}) |
4 | 3 | exbii 1493 |
. . 3
⊢ (∃z z ∈ {x ∈ A ∣ φ}
↔ ∃z z ∈ {x ∣
(x ∈
A ∧ φ)}) |
5 | 1, 4 | bitr3i 175 |
. 2
⊢ (∃x ∈ A φ ↔ ∃z z ∈ {x ∣ (x
∈ A ∧ φ)}) |
6 | | vex 2554 |
. . . . . 6
⊢ z ∈
V |
7 | 6 | snss 3485 |
. . . . 5
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} ↔
{z} ⊆ {x ∣ (x
∈ A ∧ φ)}) |
8 | | ssab2 3018 |
. . . . . 6
⊢ {x ∣ (x
∈ A ∧ φ)}
⊆ A |
9 | | sstr2 2946 |
. . . . . 6
⊢
({z} ⊆ {x ∣ (x
∈ A ∧ φ)} →
({x ∣ (x ∈ A ∧ φ)} ⊆ A → {z}
⊆ A)) |
10 | 8, 9 | mpi 15 |
. . . . 5
⊢
({z} ⊆ {x ∣ (x
∈ A ∧ φ)} →
{z} ⊆ A) |
11 | 7, 10 | sylbi 114 |
. . . 4
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} →
{z} ⊆ A) |
12 | | simpr 103 |
. . . . . . . 8
⊢
(([z / x]x ∈ A ∧ [z / x]φ) →
[z / x]φ) |
13 | | equsb1 1665 |
. . . . . . . . 9
⊢ [z / x]x = z |
14 | | elsn 3382 |
. . . . . . . . . 10
⊢ (x ∈ {z} ↔ x =
z) |
15 | 14 | sbbii 1645 |
. . . . . . . . 9
⊢
([z / x]x ∈ {z} ↔
[z / x]x = z) |
16 | 13, 15 | mpbir 134 |
. . . . . . . 8
⊢ [z / x]x ∈ {z} |
17 | 12, 16 | jctil 295 |
. . . . . . 7
⊢
(([z / x]x ∈ A ∧ [z / x]φ) →
([z / x]x ∈ {z} ∧ [z / x]φ)) |
18 | | df-clab 2024 |
. . . . . . . 8
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} ↔
[z / x](x ∈ A ∧ φ)) |
19 | | sban 1826 |
. . . . . . . 8
⊢
([z / x](x ∈ A ∧ φ) ↔
([z / x]x ∈ A ∧ [z / x]φ)) |
20 | 18, 19 | bitri 173 |
. . . . . . 7
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} ↔
([z / x]x ∈ A ∧ [z / x]φ)) |
21 | | df-rab 2309 |
. . . . . . . . 9
⊢ {x ∈ {z} ∣ φ} = {x
∣ (x ∈ {z} ∧ φ)} |
22 | 21 | eleq2i 2101 |
. . . . . . . 8
⊢ (z ∈ {x ∈ {z} ∣ φ} ↔ z ∈ {x ∣ (x
∈ {z}
∧ φ)}) |
23 | | df-clab 2024 |
. . . . . . . . 9
⊢ (z ∈ {x ∣ (x
∈ {z}
∧ φ)}
↔ [z / x](x ∈ {z} ∧ φ)) |
24 | | sban 1826 |
. . . . . . . . 9
⊢
([z / x](x ∈ {z} ∧ φ) ↔
([z / x]x ∈ {z} ∧ [z / x]φ)) |
25 | 23, 24 | bitri 173 |
. . . . . . . 8
⊢ (z ∈ {x ∣ (x
∈ {z}
∧ φ)}
↔ ([z / x]x ∈ {z} ∧ [z / x]φ)) |
26 | 22, 25 | bitri 173 |
. . . . . . 7
⊢ (z ∈ {x ∈ {z} ∣ φ} ↔ ([z / x]x ∈ {z} ∧ [z / x]φ)) |
27 | 17, 20, 26 | 3imtr4i 190 |
. . . . . 6
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} →
z ∈
{x ∈
{z} ∣ φ}) |
28 | | elex2 2564 |
. . . . . 6
⊢ (z ∈ {x ∈ {z} ∣ φ} → ∃w w ∈ {x ∈ {z} ∣ φ}) |
29 | 27, 28 | syl 14 |
. . . . 5
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} →
∃w
w ∈
{x ∈
{z} ∣ φ}) |
30 | | rabn0m 3239 |
. . . . 5
⊢ (∃w w ∈ {x ∈ {z} ∣ φ} ↔ ∃x ∈ {z}φ) |
31 | 29, 30 | sylib 127 |
. . . 4
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} →
∃x ∈ {z}φ) |
32 | | snexgOLD 3926 |
. . . . . 6
⊢ (z ∈ V →
{z} ∈
V) |
33 | 6, 32 | ax-mp 7 |
. . . . 5
⊢ {z} ∈
V |
34 | | sseq1 2960 |
. . . . . 6
⊢ (y = {z} →
(y ⊆ A ↔ {z}
⊆ A)) |
35 | | rexeq 2500 |
. . . . . 6
⊢ (y = {z} →
(∃x
∈ y φ ↔ ∃x ∈ {z}φ)) |
36 | 34, 35 | anbi12d 442 |
. . . . 5
⊢ (y = {z} →
((y ⊆ A ∧ ∃x ∈ y φ) ↔ ({z} ⊆ A
∧ ∃x ∈ {z}φ))) |
37 | 33, 36 | spcev 2641 |
. . . 4
⊢
(({z} ⊆ A ∧ ∃x ∈ {z}φ) → ∃y(y ⊆ A
∧ ∃x ∈ y φ)) |
38 | 11, 31, 37 | syl2anc 391 |
. . 3
⊢ (z ∈ {x ∣ (x
∈ A ∧ φ)} →
∃y(y ⊆
A ∧ ∃x ∈ y φ)) |
39 | 38 | exlimiv 1486 |
. 2
⊢ (∃z z ∈ {x ∣ (x
∈ A ∧ φ)} →
∃y(y ⊆
A ∧ ∃x ∈ y φ)) |
40 | 5, 39 | sylbi 114 |
1
⊢ (∃x ∈ A φ → ∃y(y ⊆ A
∧ ∃x ∈ y φ)) |