| Step | Hyp | Ref
| Expression |
| 1 | | ssrab2 4080 |
. . . . 5
⊢ {𝑥 ∈ On ∣ 𝜑} ⊆ On |
| 2 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
| 3 | | nfrab1 3457 |
. . . . . . . . 9
⊢
Ⅎ𝑥{𝑥 ∈ On ∣ 𝜑} |
| 4 | 2, 3 | nfss 3976 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} |
| 5 | 3 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑} |
| 6 | 4, 5 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}) |
| 7 | | dfss3 3972 |
. . . . . . . . 9
⊢ (𝑥 ⊆ {𝑥 ∈ On ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑}) |
| 8 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ⊆ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑})) |
| 9 | 7, 8 | bitr3id 285 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑})) |
| 10 | | rabid 3458 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑥 ∈ On ∧ 𝜑)) |
| 11 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) |
| 12 | 10, 11 | bitr3id 285 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ On ∧ 𝜑) ↔ 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) |
| 13 | 9, 12 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → (𝑥 ∈ On ∧ 𝜑)) ↔ (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}))) |
| 14 | | sbequ 2083 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
| 15 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥On |
| 16 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤On |
| 17 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤𝜑 |
| 18 | | nfs1v 2156 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
| 19 | | sbequ12 2251 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
| 20 | 15, 16, 17, 18, 19 | cbvrabw 3473 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ On ∣ 𝜑} = {𝑤 ∈ On ∣ [𝑤 / 𝑥]𝜑} |
| 21 | 14, 20 | elrab2 3695 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑦 ∈ On ∧ [𝑦 / 𝑥]𝜑)) |
| 22 | 21 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → [𝑦 / 𝑥]𝜑) |
| 23 | 22 | ralimi 3083 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → ∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑) |
| 24 | | tfis.1 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑)) |
| 25 | 23, 24 | syl5 34 |
. . . . . . . 8
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → 𝜑)) |
| 26 | 25 | anc2li 555 |
. . . . . . 7
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → (𝑥 ∈ On ∧ 𝜑))) |
| 27 | 2, 6, 13, 26 | vtoclgaf 3576 |
. . . . . 6
⊢ (𝑧 ∈ On → (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) |
| 28 | 27 | rgen 3063 |
. . . . 5
⊢
∀𝑧 ∈ On
(𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}) |
| 29 | | tfi 7874 |
. . . . 5
⊢ (({𝑥 ∈ On ∣ 𝜑} ⊆ On ∧ ∀𝑧 ∈ On (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) → {𝑥 ∈ On ∣ 𝜑} = On) |
| 30 | 1, 28, 29 | mp2an 692 |
. . . 4
⊢ {𝑥 ∈ On ∣ 𝜑} = On |
| 31 | 30 | eqcomi 2746 |
. . 3
⊢ On =
{𝑥 ∈ On ∣ 𝜑} |
| 32 | 31 | reqabi 3460 |
. 2
⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝜑)) |
| 33 | 32 | simprbi 496 |
1
⊢ (𝑥 ∈ On → 𝜑) |