| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssrab2 4079 | . . . 4
⊢ {𝑥 ∈ On ∣ 𝜑} ⊆ On | 
| 2 |  | dfss3 3971 | . . . . . . . . 9
⊢ (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} ↔ ∀𝑦 ∈ 𝑧 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑}) | 
| 3 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥On | 
| 4 | 3 | elrabsf 3833 | . . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑦 ∈ On ∧ [𝑦 / 𝑥]𝜑)) | 
| 5 | 4 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → [𝑦 / 𝑥]𝜑) | 
| 6 | 5 | ralimi 3082 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝑧 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → ∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑) | 
| 7 | 2, 6 | sylbi 217 | . . . . . . . 8
⊢ (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → ∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑) | 
| 8 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑧 | 
| 9 |  | nfsbc1v 3807 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 | 
| 10 | 8, 9 | nfralw 3310 | . . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑 | 
| 11 |  | nfsbc1v 3807 | . . . . . . . . . . 11
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 | 
| 12 | 10, 11 | nfim 1895 | . . . . . . . . . 10
⊢
Ⅎ𝑥(∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑 → [𝑧 / 𝑥]𝜑) | 
| 13 |  | raleq 3322 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑)) | 
| 14 |  | sbceq1a 3798 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | 
| 15 | 13, 14 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ↔ (∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑 → [𝑧 / 𝑥]𝜑))) | 
| 16 | 12, 15 | rspc 3609 | . . . . . . . . 9
⊢ (𝑧 ∈ On → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → (∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑 → [𝑧 / 𝑥]𝜑))) | 
| 17 | 16 | impcom 407 | . . . . . . . 8
⊢
((∀𝑥 ∈
On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ∧ 𝑧 ∈ On) → (∀𝑦 ∈ 𝑧 [𝑦 / 𝑥]𝜑 → [𝑧 / 𝑥]𝜑)) | 
| 18 | 7, 17 | syl5 34 | . . . . . . 7
⊢
((∀𝑥 ∈
On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ∧ 𝑧 ∈ On) → (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → [𝑧 / 𝑥]𝜑)) | 
| 19 |  | simpr 484 | . . . . . . 7
⊢
((∀𝑥 ∈
On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ∧ 𝑧 ∈ On) → 𝑧 ∈ On) | 
| 20 | 18, 19 | jctild 525 | . . . . . 6
⊢
((∀𝑥 ∈
On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ∧ 𝑧 ∈ On) → (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → (𝑧 ∈ On ∧ [𝑧 / 𝑥]𝜑))) | 
| 21 | 3 | elrabsf 3833 | . . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑧 ∈ On ∧ [𝑧 / 𝑥]𝜑)) | 
| 22 | 20, 21 | imbitrrdi 252 | . . . . 5
⊢
((∀𝑥 ∈
On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ∧ 𝑧 ∈ On) → (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) | 
| 23 | 22 | ralrimiva 3145 | . . . 4
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑧 ∈ On (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) | 
| 24 |  | tfi 7875 | . . . 4
⊢ (({𝑥 ∈ On ∣ 𝜑} ⊆ On ∧ ∀𝑧 ∈ On (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) → {𝑥 ∈ On ∣ 𝜑} = On) | 
| 25 | 1, 23, 24 | sylancr 587 | . . 3
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → {𝑥 ∈ On ∣ 𝜑} = On) | 
| 26 | 25 | eqcomd 2742 | . 2
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → On = {𝑥 ∈ On ∣ 𝜑}) | 
| 27 |  | rabid2 3469 | . 2
⊢ (On =
{𝑥 ∈ On ∣ 𝜑} ↔ ∀𝑥 ∈ On 𝜑) | 
| 28 | 26, 27 | sylib 218 | 1
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) |