| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | csbeq1 3901 | . . . 4
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = ⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶)) | 
| 2 |  | dfsbcq2 3790 | . . . . 5
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | 
| 3 |  | csbeq1 3901 | . . . . 5
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) | 
| 4 |  | csbeq1 3901 | . . . . 5
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑥⦌𝐶) | 
| 5 | 2, 3, 4 | ifbieq12d 4553 | . . . 4
⊢ (𝑦 = 𝐴 → if([𝑦 / 𝑥]𝜑, ⦋𝑦 / 𝑥⦌𝐵, ⦋𝑦 / 𝑥⦌𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶)) | 
| 6 | 1, 5 | eqeq12d 2752 | . . 3
⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝑦 / 𝑥]𝜑, ⦋𝑦 / 𝑥⦌𝐵, ⦋𝑦 / 𝑥⦌𝐶) ↔ ⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶))) | 
| 7 |  | vex 3483 | . . . 4
⊢ 𝑦 ∈ V | 
| 8 |  | nfs1v 2155 | . . . . 5
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 | 
| 9 |  | nfcsb1v 3922 | . . . . 5
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 | 
| 10 |  | nfcsb1v 3922 | . . . . 5
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 | 
| 11 | 8, 9, 10 | nfif 4555 | . . . 4
⊢
Ⅎ𝑥if([𝑦 / 𝑥]𝜑, ⦋𝑦 / 𝑥⦌𝐵, ⦋𝑦 / 𝑥⦌𝐶) | 
| 12 |  | sbequ12 2250 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | 
| 13 |  | csbeq1a 3912 | . . . . 5
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) | 
| 14 |  | csbeq1a 3912 | . . . . 5
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) | 
| 15 | 12, 13, 14 | ifbieq12d 4553 | . . . 4
⊢ (𝑥 = 𝑦 → if(𝜑, 𝐵, 𝐶) = if([𝑦 / 𝑥]𝜑, ⦋𝑦 / 𝑥⦌𝐵, ⦋𝑦 / 𝑥⦌𝐶)) | 
| 16 | 7, 11, 15 | csbief 3932 | . . 3
⊢
⦋𝑦 /
𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝑦 / 𝑥]𝜑, ⦋𝑦 / 𝑥⦌𝐵, ⦋𝑦 / 𝑥⦌𝐶) | 
| 17 | 6, 16 | vtoclg 3553 | . 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶)) | 
| 18 |  | csbprc 4408 | . . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = ∅) | 
| 19 |  | csbprc 4408 | . . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ∅) | 
| 20 |  | csbprc 4408 | . . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐶 = ∅) | 
| 21 | 19, 20 | ifeq12d 4546 | . . . 4
⊢ (¬
𝐴 ∈ V →
if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶) = if([𝐴 / 𝑥]𝜑, ∅, ∅)) | 
| 22 |  | ifid 4565 | . . . 4
⊢
if([𝐴 / 𝑥]𝜑, ∅, ∅) =
∅ | 
| 23 | 21, 22 | eqtr2di 2793 | . . 3
⊢ (¬
𝐴 ∈ V → ∅ =
if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶)) | 
| 24 | 18, 23 | eqtrd 2776 | . 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶)) | 
| 25 | 17, 24 | pm2.61i 182 | 1
⊢
⦋𝐴 /
𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶) |