| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqeq2 2748 | . . . . . 6
⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) | 
| 2 | 1 | imbi2d 340 | . . . . 5
⊢ (𝑦 = 𝐴 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜑 → 𝑥 = 𝐴))) | 
| 3 | 2 | albidv 1919 | . . . 4
⊢ (𝑦 = 𝐴 → (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝜑 → 𝑥 = 𝐴))) | 
| 4 |  | dfsbcq 3789 | . . . . 5
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | 
| 5 | 4 | bibi1d 343 | . . . 4
⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ↔ ∃𝑥𝜑) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥𝜑))) | 
| 6 | 3, 5 | imbi12d 344 | . . 3
⊢ (𝑦 = 𝐴 → ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥𝜑)) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥𝜑)))) | 
| 7 |  | sbc5 3815 | . . . 4
⊢
([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | 
| 8 |  | nfa1 2150 | . . . . 5
⊢
Ⅎ𝑥∀𝑥(𝜑 → 𝑥 = 𝑦) | 
| 9 |  | simpr 484 | . . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑) | 
| 10 |  | ancr 546 | . . . . . . 7
⊢ ((𝜑 → 𝑥 = 𝑦) → (𝜑 → (𝑥 = 𝑦 ∧ 𝜑))) | 
| 11 | 10 | sps 2184 | . . . . . 6
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑦) → (𝜑 → (𝑥 = 𝑦 ∧ 𝜑))) | 
| 12 | 9, 11 | impbid2 226 | . . . . 5
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑦) → ((𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜑)) | 
| 13 | 8, 12 | exbid 2222 | . . . 4
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥𝜑)) | 
| 14 | 7, 13 | bitrid 283 | . . 3
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥𝜑)) | 
| 15 | 6, 14 | vtoclg 3553 | . 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 → 𝑥 = 𝐴) → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥𝜑))) | 
| 16 | 15 | pm5.32d 577 | 1
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) |