| Step | Hyp | Ref
| Expression |
| 1 | | csbab 4440 |
. . 3
⊢
⦋𝐴 /
𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} |
| 2 | | sbcex2 3850 |
. . . . 5
⊢
([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
| 3 | | sbcex2 3850 |
. . . . . . 7
⊢
([𝐴 / 𝑥]∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
| 4 | | sbcan 3838 |
. . . . . . . . 9
⊢
([𝐴 / 𝑥](𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
| 5 | | sbcg 3863 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ↔ 𝑧 = 〈𝑤, 𝑦〉)) |
| 6 | | sbcan 3838 |
. . . . . . . . . . . . 13
⊢
([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶)) |
| 7 | | sbcel2 4418 |
. . . . . . . . . . . . . 14
⊢
([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵) |
| 8 | | sbcel2 4418 |
. . . . . . . . . . . . . 14
⊢
([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) |
| 9 | 7, 8 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢
(([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
| 10 | 6, 9 | bitri 275 |
. . . . . . . . . . . 12
⊢
([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
| 11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 12 | 5, 11 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))) |
| 13 | | sbcex 3798 |
. . . . . . . . . . . . 13
⊢
([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ V) |
| 14 | 13 | con3i 154 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V → ¬
[𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
| 15 | 14 | intnand 488 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V → ¬
([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
| 16 | | noel 4338 |
. . . . . . . . . . . . . . 15
⊢ ¬
𝑦 ∈
∅ |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ V → ¬
𝑦 ∈
∅) |
| 18 | | csbprc 4409 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐶 = ∅) |
| 19 | 17, 18 | neleqtrrd 2864 |
. . . . . . . . . . . . 13
⊢ (¬
𝐴 ∈ V → ¬
𝑦 ∈
⦋𝐴 / 𝑥⦌𝐶) |
| 20 | 19 | intnand 488 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V → ¬
(𝑤 ∈
⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)) |
| 21 | 20 | intnand 488 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V → ¬
(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 22 | 15, 21 | 2falsed 376 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ V →
(([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))) |
| 23 | 12, 22 | pm2.61i 182 |
. . . . . . . . 9
⊢
(([𝐴 / 𝑥]𝑧 = 〈𝑤, 𝑦〉 ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 24 | 4, 23 | bitri 275 |
. . . . . . . 8
⊢
([𝐴 / 𝑥](𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 25 | 24 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑦[𝐴 / 𝑥](𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 26 | 3, 25 | bitri 275 |
. . . . . 6
⊢
([𝐴 / 𝑥]∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 27 | 26 | exbii 1848 |
. . . . 5
⊢
(∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 28 | 2, 27 | bitri 275 |
. . . 4
⊢
([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))) |
| 29 | 28 | abbii 2809 |
. . 3
⊢ {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))} |
| 30 | 1, 29 | eqtri 2765 |
. 2
⊢
⦋𝐴 /
𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))} |
| 31 | | df-xp 5691 |
. . . 4
⊢ (𝐵 × 𝐶) = {〈𝑤, 𝑦〉 ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} |
| 32 | | df-opab 5206 |
. . . 4
⊢
{〈𝑤, 𝑦〉 ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} |
| 33 | 31, 32 | eqtri 2765 |
. . 3
⊢ (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} |
| 34 | 33 | csbeq2i 3907 |
. 2
⊢
⦋𝐴 /
𝑥⦌(𝐵 × 𝐶) = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} |
| 35 | | df-xp 5691 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {〈𝑤, 𝑦〉 ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} |
| 36 | | df-opab 5206 |
. . 3
⊢
{〈𝑤, 𝑦〉 ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))} |
| 37 | 35, 36 | eqtri 2765 |
. 2
⊢
(⦋𝐴 /
𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = 〈𝑤, 𝑦〉 ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))} |
| 38 | 30, 34, 37 | 3eqtr4i 2775 |
1
⊢
⦋𝐴 /
𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) |