| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | csbab 4439 | . . . 4
⊢
⦋𝐴 /
𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} | 
| 2 |  | sbcex2 3849 | . . . . . 6
⊢
([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | 
| 3 |  | sbcan 3837 | . . . . . . . 8
⊢
([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵)) | 
| 4 |  | sbcg 3862 | . . . . . . . . . 10
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)) | 
| 5 | 4 | anbi1d 631 | . . . . . . . . 9
⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵))) | 
| 6 |  | sbcel2 4417 | . . . . . . . . . 10
⊢
([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵) | 
| 7 | 6 | anbi2i 623 | . . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)) | 
| 8 | 5, 7 | bitrdi 287 | . . . . . . . 8
⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) | 
| 9 | 3, 8 | bitrid 283 | . . . . . . 7
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) | 
| 10 | 9 | exbidv 1920 | . . . . . 6
⊢ (𝐴 ∈ V → (∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) | 
| 11 | 2, 10 | bitrid 283 | . . . . 5
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) | 
| 12 | 11 | abbidv 2807 | . . . 4
⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}) | 
| 13 | 1, 12 | eqtrid 2788 | . . 3
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}) | 
| 14 |  | df-uni 4907 | . . . 4
⊢ ∪ 𝐵 =
{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} | 
| 15 | 14 | csbeq2i 3906 | . . 3
⊢
⦋𝐴 /
𝑥⦌∪ 𝐵 =
⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} | 
| 16 |  | df-uni 4907 | . . 3
⊢ ∪ ⦋𝐴 / 𝑥⦌𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)} | 
| 17 | 13, 15, 16 | 3eqtr4g 2801 | . 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵) | 
| 18 |  | csbprc 4408 | . . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∅) | 
| 19 |  | csbprc 4408 | . . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ∅) | 
| 20 | 19 | unieqd 4919 | . . . 4
⊢ (¬
𝐴 ∈ V → ∪ ⦋𝐴 / 𝑥⦌𝐵 = ∪
∅) | 
| 21 |  | uni0 4934 | . . . 4
⊢ ∪ ∅ = ∅ | 
| 22 | 20, 21 | eqtr2di 2793 | . . 3
⊢ (¬
𝐴 ∈ V → ∅ =
∪ ⦋𝐴 / 𝑥⦌𝐵) | 
| 23 | 18, 22 | eqtrd 2776 | . 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵) | 
| 24 | 17, 23 | pm2.61i 182 | 1
⊢
⦋𝐴 /
𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵 |