| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ancrb 547 | . . 3
⊢ ((𝜑 → 𝑥 ∈ 𝐴) ↔ (𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | 
| 2 | 1 | albii 1819 | . 2
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | 
| 3 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑦(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) | 
| 4 |  | nfsab1 2722 | . . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | 
| 5 |  | nfrab1 3457 | . . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} | 
| 6 | 5 | nfcri 2897 | . . . 4
⊢
Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} | 
| 7 | 4, 6 | nfim 1896 | . . 3
⊢
Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | 
| 8 |  | abid 2718 | . . . . 5
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | 
| 9 |  | eleq1w 2824 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) | 
| 10 | 8, 9 | bitr3id 285 | . . . 4
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})) | 
| 11 |  | rabid 3458 | . . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | 
| 12 |  | eleq1w 2824 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 13 | 11, 12 | bitr3id 285 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 14 | 10, 13 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}))) | 
| 15 | 3, 7, 14 | cbvalv1 2343 | . 2
⊢
(∀𝑥(𝜑 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 16 |  | eqss 3999 | . . 3
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 17 |  | rabssab 4085 | . . . 4
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} | 
| 18 | 17 | biantrur 530 | . . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} ∧ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 19 |  | df-ss 3968 | . . 3
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) | 
| 20 | 16, 18, 19 | 3bitr2ri 300 | . 2
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | 
| 21 | 2, 15, 20 | 3bitri 297 | 1
⊢
(∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) |