Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧𝑋 |
2 | 1 | nfcri 2745 |
. . . . 5
⊢
Ⅎ𝑧 𝑥 ∈ 𝑋 |
3 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑧∃𝑦 ∈ 𝑌 𝜑 |
4 | 2, 3 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑧(𝑥 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 𝜑) |
5 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝑋 |
6 | 5 | nfcri 2745 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ 𝑋 |
7 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝑌 |
8 | | nfs1v 2425 |
. . . . . 6
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
9 | 7, 8 | nfrex 2990 |
. . . . 5
⊢
Ⅎ𝑥∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑 |
10 | 6, 9 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑥(𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑) |
11 | | eleq1 2676 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑋 ↔ 𝑧 ∈ 𝑋)) |
12 | | sbequ12 2097 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
13 | 12 | rexbidv 3034 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝑌 𝜑 ↔ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑)) |
14 | 11, 13 | anbi12d 743 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 𝜑) ↔ (𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑))) |
15 | 4, 10, 14 | cbvab 2733 |
. . 3
⊢ {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑)} |
16 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
17 | 16, 5, 8, 12 | elrabf 3329 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑} ↔ (𝑧 ∈ 𝑋 ∧ [𝑧 / 𝑥]𝜑)) |
18 | 17 | rexbii 3023 |
. . . . 5
⊢
(∃𝑦 ∈
𝑌 𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑} ↔ ∃𝑦 ∈ 𝑌 (𝑧 ∈ 𝑋 ∧ [𝑧 / 𝑥]𝜑)) |
19 | | r19.42v 3073 |
. . . . 5
⊢
(∃𝑦 ∈
𝑌 (𝑧 ∈ 𝑋 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑)) |
20 | 18, 19 | bitr2i 264 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑) ↔ ∃𝑦 ∈ 𝑌 𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑}) |
21 | 20 | abbii 2726 |
. . 3
⊢ {𝑧 ∣ (𝑧 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 [𝑧 / 𝑥]𝜑)} = {𝑧 ∣ ∃𝑦 ∈ 𝑌 𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑}} |
22 | 15, 21 | eqtri 2632 |
. 2
⊢ {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 𝜑)} = {𝑧 ∣ ∃𝑦 ∈ 𝑌 𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑}} |
23 | | df-rab 2905 |
. 2
⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑌 𝜑)} |
24 | | df-iun 4457 |
. 2
⊢ ∪ 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ 𝜑} = {𝑧 ∣ ∃𝑦 ∈ 𝑌 𝑧 ∈ {𝑥 ∈ 𝑋 ∣ 𝜑}} |
25 | 22, 23, 24 | 3eqtr4i 2642 |
1
⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 𝜑} = ∪
𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ 𝜑} |