| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-scott 44260 | . 2
⊢ Scott
{𝑥 ∣ 𝜑} = {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} | 
| 2 |  | df-rab 3436 | . 2
⊢ {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} = {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} | 
| 3 |  | eqabcb 2882 | . . 3
⊢ ({𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑧((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))})) | 
| 4 |  | nfsab1 2721 | . . . . . 6
⊢
Ⅎ𝑥 𝑧 ∈ {𝑥 ∣ 𝜑} | 
| 5 |  | nfab1 2906 | . . . . . . 7
⊢
Ⅎ𝑥{𝑥 ∣ 𝜑} | 
| 6 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤) | 
| 7 | 5, 6 | nfralw 3310 | . . . . . 6
⊢
Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) | 
| 8 | 4, 7 | nfan 1898 | . . . . 5
⊢
Ⅎ𝑥(𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) | 
| 9 |  | vex 3483 | . . . . 5
⊢ 𝑧 ∈ V | 
| 10 |  | abid 2717 | . . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | 
| 11 |  | eleq1w 2823 | . . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ 𝜑})) | 
| 12 | 10, 11 | bitr3id 285 | . . . . . 6
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝑧 ∈ {𝑥 ∣ 𝜑})) | 
| 13 |  | df-clab 2714 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | 
| 14 |  | scottabf.1 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜓 | 
| 15 |  | scottabf.2 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | 
| 16 | 14, 15 | sbiev 2313 | . . . . . . . . . . . 12
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | 
| 17 | 13, 16 | bitr2i 276 | . . . . . . . . . . 11
⊢ (𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑}) | 
| 18 |  | eleq1w 2823 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) | 
| 19 | 17, 18 | bitrid 283 | . . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) | 
| 20 | 19 | adantl 481 | . . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) | 
| 21 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧) | 
| 22 | 21 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧)) | 
| 23 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) | 
| 24 | 23 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤)) | 
| 25 | 22, 24 | sseq12d 4016 | . . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤))) | 
| 26 | 20, 25 | imbi12d 344 | . . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))) | 
| 27 | 26 | cbvaldvaw 2036 | . . . . . . 7
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))) | 
| 28 |  | df-ral 3061 | . . . . . . 7
⊢
(∀𝑤 ∈
{𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))) | 
| 29 | 27, 28 | bitr4di 289 | . . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))) | 
| 30 | 12, 29 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))) | 
| 31 | 8, 9, 30 | elabf 3674 | . . . 4
⊢ (𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))) | 
| 32 | 31 | bicomi 224 | . . 3
⊢ ((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}) | 
| 33 | 3, 32 | mpgbir 1798 | . 2
⊢ {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | 
| 34 | 1, 2, 33 | 3eqtri 2768 | 1
⊢ Scott
{𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} |