Step | Hyp | Ref
| Expression |
1 | | elex 2566 |
. 2
⊢
(〈𝑥, 𝐶〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 〈𝑥, 𝐶〉 ∈ V) |
2 | | vex 2560 |
. . 3
⊢ 𝑥 ∈ V |
3 | | elex 2566 |
. . . 4
⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ V) |
4 | 3 | adantl 262 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ V) |
5 | | opexgOLD 3965 |
. . 3
⊢ ((𝑥 ∈ V ∧ 𝐶 ∈ V) → 〈𝑥, 𝐶〉 ∈ V) |
6 | 2, 4, 5 | sylancr 393 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 〈𝑥, 𝐶〉 ∈ V) |
7 | | df-rex 2312 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) |
8 | | nfv 1421 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) |
9 | | nfs1v 1815 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝑥 ∈ 𝐴 |
10 | | nfcv 2178 |
. . . . . . . . . 10
⊢
Ⅎ𝑥{𝑧} |
11 | | nfcsb1v 2882 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
12 | 10, 11 | nfxp 4371 |
. . . . . . . . 9
⊢
Ⅎ𝑥({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
13 | 12 | nfcri 2172 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
14 | 9, 13 | nfan 1457 |
. . . . . . 7
⊢
Ⅎ𝑥([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) |
15 | | sbequ12 1654 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑥 ∈ 𝐴)) |
16 | | sneq 3386 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
17 | | csbeq1a 2860 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
18 | 16, 17 | xpeq12d 4370 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) |
19 | 18 | eleq2d 2107 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵))) |
20 | 15, 19 | anbi12d 442 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)))) |
21 | 8, 14, 20 | cbvex 1639 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵))) |
22 | 7, 21 | bitri 173 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵))) |
23 | | eleq1 2100 |
. . . . . . 7
⊢ (𝑦 = 〈𝑥, 𝐶〉 → (𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↔ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵))) |
24 | 23 | anbi2d 437 |
. . . . . 6
⊢ (𝑦 = 〈𝑥, 𝐶〉 → (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)))) |
25 | 24 | exbidv 1706 |
. . . . 5
⊢ (𝑦 = 〈𝑥, 𝐶〉 → (∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ ∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)))) |
26 | 22, 25 | syl5bb 181 |
. . . 4
⊢ (𝑦 = 〈𝑥, 𝐶〉 → (∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)))) |
27 | | df-iun 3659 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)} |
28 | 26, 27 | elab2g 2689 |
. . 3
⊢
(〈𝑥, 𝐶〉 ∈ V →
(〈𝑥, 𝐶〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)))) |
29 | | opelxp 4374 |
. . . . . . 7
⊢
(〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↔ (𝑥 ∈ {𝑧} ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
30 | 29 | anbi2i 430 |
. . . . . 6
⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
31 | | an12 495 |
. . . . . 6
⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ (𝑥 ∈ {𝑧} ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵)) ↔ (𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
32 | | velsn 3392 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧) |
33 | | equcom 1593 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
34 | 32, 33 | bitri 173 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑧} ↔ 𝑧 = 𝑥) |
35 | 34 | anbi1i 431 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑧} ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
36 | 30, 31, 35 | 3bitri 195 |
. . . . 5
⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ (𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
37 | 36 | exbii 1496 |
. . . 4
⊢
(∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ ∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
38 | | sbequ12r 1655 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
39 | 17 | equcoms 1594 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
40 | 39 | eqcomd 2045 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐵) |
41 | 40 | eleq2d 2107 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↔ 𝐶 ∈ 𝐵)) |
42 | 38, 41 | anbi12d 442 |
. . . . 5
⊢ (𝑧 = 𝑥 → (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) |
43 | 2, 42 | ceqsexv 2593 |
. . . 4
⊢
(∃𝑧(𝑧 = 𝑥 ∧ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋𝑧 / 𝑥⦌𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) |
44 | 37, 43 | bitri 173 |
. . 3
⊢
(∃𝑧([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝐶〉 ∈ ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) |
45 | 28, 44 | syl6bb 185 |
. 2
⊢
(〈𝑥, 𝐶〉 ∈ V →
(〈𝑥, 𝐶〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) |
46 | 1, 6, 45 | pm5.21nii 620 |
1
⊢
(〈𝑥, 𝐶〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) |