Step | Hyp | Ref
| Expression |
1 | | eqeq1 2359 |
. . . . . . . . . 10
⊢ (z = x →
(z = A
↔ x = A)) |
2 | 1 | anbi2d 684 |
. . . . . . . . 9
⊢ (z = x →
((φ ∧
z = A)
↔ (φ ∧ x = A))) |
3 | 2 | exbidv 1626 |
. . . . . . . 8
⊢ (z = x →
(∃y(φ ∧ z = A) ↔ ∃y(φ ∧ x = A))) |
4 | 3 | cbvabv 2472 |
. . . . . . 7
⊢ {z ∣ ∃y(φ ∧ z = A)} =
{x ∣
∃y(φ ∧ x = A)} |
5 | | intab.2 |
. . . . . . 7
⊢ {x ∣ ∃y(φ ∧ x = A)} ∈ V |
6 | 4, 5 | eqeltri 2423 |
. . . . . 6
⊢ {z ∣ ∃y(φ ∧ z = A)} ∈ V |
7 | | nfe1 1732 |
. . . . . . . . 9
⊢ Ⅎy∃y(φ ∧ z = A) |
8 | 7 | nfab 2493 |
. . . . . . . 8
⊢
Ⅎy{z ∣ ∃y(φ ∧ z = A)} |
9 | 8 | nfeq2 2500 |
. . . . . . 7
⊢ Ⅎy x = {z ∣ ∃y(φ ∧ z = A)} |
10 | | eleq2 2414 |
. . . . . . . 8
⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → (A
∈ x
↔ A ∈ {z ∣ ∃y(φ ∧ z = A)})) |
11 | 10 | imbi2d 307 |
. . . . . . 7
⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → ((φ → A ∈ x) ↔ (φ
→ A ∈ {z ∣ ∃y(φ ∧ z = A)}))) |
12 | 9, 11 | albid 1772 |
. . . . . 6
⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → (∀y(φ → A ∈ x) ↔ ∀y(φ → A ∈ {z ∣ ∃y(φ ∧ z = A)}))) |
13 | 6, 12 | elab 2985 |
. . . . 5
⊢ ({z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ →
A ∈
x)} ↔ ∀y(φ → A ∈ {z ∣ ∃y(φ ∧ z = A)})) |
14 | | 19.8a 1756 |
. . . . . . . . 9
⊢ ((φ ∧ z = A) →
∃y(φ ∧ z = A)) |
15 | 14 | ex 423 |
. . . . . . . 8
⊢ (φ → (z = A →
∃y(φ ∧ z = A))) |
16 | 15 | alrimiv 1631 |
. . . . . . 7
⊢ (φ → ∀z(z = A →
∃y(φ ∧ z = A))) |
17 | | intab.1 |
. . . . . . . 8
⊢ A ∈
V |
18 | 17 | sbc6 3072 |
. . . . . . 7
⊢ ([̣A / z]̣∃y(φ ∧ z = A) ↔ ∀z(z = A →
∃y(φ ∧ z = A))) |
19 | 16, 18 | sylibr 203 |
. . . . . 6
⊢ (φ → [̣A / z]̣∃y(φ ∧ z = A)) |
20 | | df-sbc 3047 |
. . . . . 6
⊢ ([̣A / z]̣∃y(φ ∧ z = A) ↔ A
∈ {z
∣ ∃y(φ ∧ z = A)}) |
21 | 19, 20 | sylib 188 |
. . . . 5
⊢ (φ → A ∈ {z ∣ ∃y(φ ∧ z = A)}) |
22 | 13, 21 | mpgbir 1550 |
. . . 4
⊢ {z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ →
A ∈
x)} |
23 | | intss1 3941 |
. . . 4
⊢ ({z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ →
A ∈
x)} → ∩{x ∣ ∀y(φ →
A ∈
x)} ⊆
{z ∣
∃y(φ ∧ z = A)}) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ ∩{x ∣ ∀y(φ →
A ∈
x)} ⊆
{z ∣
∃y(φ ∧ z = A)} |
25 | | 19.29r 1597 |
. . . . . . . 8
⊢ ((∃y(φ ∧ z = A) ∧ ∀y(φ →
A ∈
x)) → ∃y((φ ∧ z = A) ∧ (φ →
A ∈
x))) |
26 | | simplr 731 |
. . . . . . . . . 10
⊢ (((φ ∧ z = A) ∧ (φ →
A ∈
x)) → z = A) |
27 | | pm3.35 570 |
. . . . . . . . . . 11
⊢ ((φ ∧ (φ → A ∈ x)) → A
∈ x) |
28 | 27 | adantlr 695 |
. . . . . . . . . 10
⊢ (((φ ∧ z = A) ∧ (φ →
A ∈
x)) → A ∈ x) |
29 | 26, 28 | eqeltrd 2427 |
. . . . . . . . 9
⊢ (((φ ∧ z = A) ∧ (φ →
A ∈
x)) → z ∈ x) |
30 | 29 | exlimiv 1634 |
. . . . . . . 8
⊢ (∃y((φ ∧ z = A) ∧ (φ →
A ∈
x)) → z ∈ x) |
31 | 25, 30 | syl 15 |
. . . . . . 7
⊢ ((∃y(φ ∧ z = A) ∧ ∀y(φ →
A ∈
x)) → z ∈ x) |
32 | 31 | ex 423 |
. . . . . 6
⊢ (∃y(φ ∧ z = A) →
(∀y(φ →
A ∈
x) → z ∈ x)) |
33 | 32 | alrimiv 1631 |
. . . . 5
⊢ (∃y(φ ∧ z = A) →
∀x(∀y(φ →
A ∈
x) → z ∈ x)) |
34 | | vex 2862 |
. . . . . 6
⊢ z ∈
V |
35 | 34 | elintab 3937 |
. . . . 5
⊢ (z ∈ ∩{x ∣ ∀y(φ →
A ∈
x)} ↔ ∀x(∀y(φ → A ∈ x) → z
∈ x)) |
36 | 33, 35 | sylibr 203 |
. . . 4
⊢ (∃y(φ ∧ z = A) →
z ∈ ∩{x ∣ ∀y(φ →
A ∈
x)}) |
37 | 36 | abssi 3341 |
. . 3
⊢ {z ∣ ∃y(φ ∧ z = A)} ⊆ ∩{x ∣ ∀y(φ → A ∈ x)} |
38 | 24, 37 | eqssi 3288 |
. 2
⊢ ∩{x ∣ ∀y(φ →
A ∈
x)} = {z ∣ ∃y(φ ∧ z = A)} |
39 | 38, 4 | eqtri 2373 |
1
⊢ ∩{x ∣ ∀y(φ →
A ∈
x)} = {x ∣ ∃y(φ ∧ x = A)} |