| Step | Hyp | Ref
| Expression |
| 1 | | df-iun 4993 |
. . 3
⊢ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 ∈ (𝐴 × {𝑦})} |
| 2 | 1 | eleq2i 2833 |
. 2
⊢
(〈𝐶, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ 〈𝐶, 𝑦〉 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 ∈ (𝐴 × {𝑦})}) |
| 3 | | opex 5469 |
. . 3
⊢
〈𝐶, 𝑦〉 ∈ V |
| 4 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 𝑥 ∈ (𝐴 × {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 × {𝑦}))) |
| 5 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧(𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 × {𝑦})) |
| 6 | | nfs1v 2156 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑧 / 𝑦]𝑦 ∈ 𝐵 |
| 7 | | nfcsb1v 3923 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐴 |
| 8 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑦{𝑧} |
| 9 | 7, 8 | nfxp 5718 |
. . . . . . . 8
⊢
Ⅎ𝑦(⦋𝑧 / 𝑦⦌𝐴 × {𝑧}) |
| 10 | 9 | nfcri 2897 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}) |
| 11 | 6, 10 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑦([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) |
| 12 | | sbequ12 2251 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ [𝑧 / 𝑦]𝑦 ∈ 𝐵)) |
| 13 | | csbeq1a 3913 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → 𝐴 = ⦋𝑧 / 𝑦⦌𝐴) |
| 14 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
| 15 | 13, 14 | xpeq12d 5716 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐴 × {𝑦}) = (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) |
| 16 | 15 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑥 ∈ (𝐴 × {𝑦}) ↔ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}))) |
| 17 | 12, 16 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 × {𝑦})) ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})))) |
| 18 | 5, 11, 17 | cbvexv1 2344 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 × {𝑦})) ↔ ∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}))) |
| 19 | 4, 18 | bitri 275 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝑥 ∈ (𝐴 × {𝑦}) ↔ ∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}))) |
| 20 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 〈𝐶, 𝑦〉 → (𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}) ↔ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}))) |
| 21 | 20 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 〈𝐶, 𝑦〉 → (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})))) |
| 22 | 21 | exbidv 1921 |
. . . 4
⊢ (𝑥 = 〈𝐶, 𝑦〉 → (∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝑥 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ ∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})))) |
| 23 | 19, 22 | bitrid 283 |
. . 3
⊢ (𝑥 = 〈𝐶, 𝑦〉 → (∃𝑦 ∈ 𝐵 𝑥 ∈ (𝐴 × {𝑦}) ↔ ∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})))) |
| 24 | 3, 23 | elab 3679 |
. 2
⊢
(〈𝐶, 𝑦〉 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 ∈ (𝐴 × {𝑦})} ↔ ∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧}))) |
| 25 | | opelxp 5721 |
. . . . . 6
⊢
(〈𝐶, 𝑦〉 ∈
(⦋𝑧 / 𝑦⦌𝐴 × {𝑧}) ↔ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ 𝑦 ∈ {𝑧})) |
| 26 | 25 | anbi2i 623 |
. . . . 5
⊢ (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ 𝑦 ∈ {𝑧}))) |
| 27 | | an13 647 |
. . . . . 6
⊢ (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ 𝑦 ∈ {𝑧})) ↔ (𝑦 ∈ {𝑧} ∧ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ [𝑧 / 𝑦]𝑦 ∈ 𝐵))) |
| 28 | | ancom 460 |
. . . . . . 7
⊢ ((𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ [𝑧 / 𝑦]𝑦 ∈ 𝐵) ↔ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴)) |
| 29 | 28 | anbi2i 623 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑧} ∧ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ [𝑧 / 𝑦]𝑦 ∈ 𝐵)) ↔ (𝑦 ∈ {𝑧} ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴))) |
| 30 | 27, 29 | bitri 275 |
. . . . 5
⊢ (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ∧ 𝑦 ∈ {𝑧})) ↔ (𝑦 ∈ {𝑧} ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴))) |
| 31 | | velsn 4642 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧) |
| 32 | | equcom 2017 |
. . . . . . 7
⊢ (𝑦 = 𝑧 ↔ 𝑧 = 𝑦) |
| 33 | 31, 32 | bitri 275 |
. . . . . 6
⊢ (𝑦 ∈ {𝑧} ↔ 𝑧 = 𝑦) |
| 34 | 33 | anbi1i 624 |
. . . . 5
⊢ ((𝑦 ∈ {𝑧} ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴)) ↔ (𝑧 = 𝑦 ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴))) |
| 35 | 26, 30, 34 | 3bitri 297 |
. . . 4
⊢ (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ (𝑧 = 𝑦 ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴))) |
| 36 | 35 | exbii 1848 |
. . 3
⊢
(∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ ∃𝑧(𝑧 = 𝑦 ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴))) |
| 37 | | sbequ12r 2252 |
. . . . 5
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
| 38 | 13 | equcoms 2019 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → 𝐴 = ⦋𝑧 / 𝑦⦌𝐴) |
| 39 | 38 | eqcomd 2743 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ⦋𝑧 / 𝑦⦌𝐴 = 𝐴) |
| 40 | 39 | eleq2d 2827 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴 ↔ 𝐶 ∈ 𝐴)) |
| 41 | 37, 40 | anbi12d 632 |
. . . 4
⊢ (𝑧 = 𝑦 → (([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))) |
| 42 | 41 | equsexvw 2004 |
. . 3
⊢
(∃𝑧(𝑧 = 𝑦 ∧ ([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋𝑧 / 𝑦⦌𝐴)) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) |
| 43 | 36, 42 | bitri 275 |
. 2
⊢
(∃𝑧([𝑧 / 𝑦]𝑦 ∈ 𝐵 ∧ 〈𝐶, 𝑦〉 ∈ (⦋𝑧 / 𝑦⦌𝐴 × {𝑧})) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) |
| 44 | 2, 24, 43 | 3bitri 297 |
1
⊢
(〈𝐶, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) |