Step | Hyp | Ref
| Expression |
1 | | ssrab2 3019 |
. . . . 5
⊢ {x ∈ On ∣
φ} ⊆ On |
2 | | nfcv 2175 |
. . . . . . 7
⊢
Ⅎxz |
3 | | nfrab1 2483 |
. . . . . . . . 9
⊢
Ⅎx{x ∈ On ∣
φ} |
4 | 2, 3 | nfss 2932 |
. . . . . . . 8
⊢
Ⅎx z ⊆ {x
∈ On ∣ φ} |
5 | 3 | nfcri 2169 |
. . . . . . . 8
⊢
Ⅎx z ∈ {x ∈ On ∣
φ} |
6 | 4, 5 | nfim 1461 |
. . . . . . 7
⊢
Ⅎx(z ⊆ {x
∈ On ∣ φ} → z ∈ {x ∈ On ∣
φ}) |
7 | | dfss3 2929 |
. . . . . . . . 9
⊢ (x ⊆ {x
∈ On ∣ φ} ↔ ∀y ∈ x y ∈ {x ∈ On ∣
φ}) |
8 | | sseq1 2960 |
. . . . . . . . 9
⊢ (x = z →
(x ⊆ {x ∈ On ∣
φ} ↔ z ⊆ {x
∈ On ∣ φ})) |
9 | 7, 8 | syl5bbr 183 |
. . . . . . . 8
⊢ (x = z →
(∀y
∈ x
y ∈
{x ∈ On
∣ φ} ↔ z ⊆ {x
∈ On ∣ φ})) |
10 | | rabid 2479 |
. . . . . . . . 9
⊢ (x ∈ {x ∈ On ∣
φ} ↔ (x ∈ On ∧ φ)) |
11 | | eleq1 2097 |
. . . . . . . . 9
⊢ (x = z →
(x ∈
{x ∈ On
∣ φ} ↔ z ∈ {x ∈ On ∣
φ})) |
12 | 10, 11 | syl5bbr 183 |
. . . . . . . 8
⊢ (x = z →
((x ∈ On
∧ φ)
↔ z ∈ {x ∈ On ∣ φ})) |
13 | 9, 12 | imbi12d 223 |
. . . . . . 7
⊢ (x = z →
((∀y
∈ x
y ∈
{x ∈ On
∣ φ} → (x ∈ On ∧ φ)) ↔
(z ⊆ {x ∈ On ∣
φ} → z ∈ {x ∈ On ∣
φ}))) |
14 | | sbequ 1718 |
. . . . . . . . . . . 12
⊢ (w = y →
([w / x]φ ↔
[y / x]φ)) |
15 | | nfcv 2175 |
. . . . . . . . . . . . 13
⊢
ℲxOn |
16 | | nfcv 2175 |
. . . . . . . . . . . . 13
⊢
ℲwOn |
17 | | nfv 1418 |
. . . . . . . . . . . . 13
⊢
Ⅎwφ |
18 | | nfs1v 1812 |
. . . . . . . . . . . . 13
⊢
Ⅎx[w / x]φ |
19 | | sbequ12 1651 |
. . . . . . . . . . . . 13
⊢ (x = w →
(φ ↔ [w / x]φ)) |
20 | 15, 16, 17, 18, 19 | cbvrab 2549 |
. . . . . . . . . . . 12
⊢ {x ∈ On ∣
φ} = {w ∈ On ∣
[w / x]φ} |
21 | 14, 20 | elrab2 2694 |
. . . . . . . . . . 11
⊢ (y ∈ {x ∈ On ∣
φ} ↔ (y ∈ On ∧ [y / x]φ)) |
22 | 21 | simprbi 260 |
. . . . . . . . . 10
⊢ (y ∈ {x ∈ On ∣
φ} → [y / x]φ) |
23 | 22 | ralimi 2378 |
. . . . . . . . 9
⊢ (∀y ∈ x y ∈ {x ∈ On ∣
φ} → ∀y ∈ x [y / x]φ) |
24 | | tfis.1 |
. . . . . . . . 9
⊢ (x ∈ On →
(∀y
∈ x
[y / x]φ →
φ)) |
25 | 23, 24 | syl5 28 |
. . . . . . . 8
⊢ (x ∈ On →
(∀y
∈ x
y ∈
{x ∈ On
∣ φ} → φ)) |
26 | 25 | anc2li 312 |
. . . . . . 7
⊢ (x ∈ On →
(∀y
∈ x
y ∈
{x ∈ On
∣ φ} → (x ∈ On ∧ φ))) |
27 | 2, 6, 13, 26 | vtoclgaf 2612 |
. . . . . 6
⊢ (z ∈ On →
(z ⊆ {x ∈ On ∣
φ} → z ∈ {x ∈ On ∣
φ})) |
28 | 27 | rgen 2368 |
. . . . 5
⊢ ∀z ∈ On (z ⊆
{x ∈ On
∣ φ} → z ∈ {x ∈ On ∣
φ}) |
29 | | tfi 4248 |
. . . . 5
⊢
(({x ∈ On ∣ φ} ⊆ On ∧ ∀z ∈ On (z ⊆ {x
∈ On ∣ φ} → z ∈ {x ∈ On ∣
φ})) → {x ∈ On ∣
φ} = On) |
30 | 1, 28, 29 | mp2an 402 |
. . . 4
⊢ {x ∈ On ∣
φ} = On |
31 | 30 | eqcomi 2041 |
. . 3
⊢ On =
{x ∈ On
∣ φ} |
32 | 31 | rabeq2i 2548 |
. 2
⊢ (x ∈ On ↔
(x ∈ On
∧ φ)) |
33 | 32 | simprbi 260 |
1
⊢ (x ∈ On →
φ) |