Step | Hyp | Ref
| Expression |
1 | | df-rex 2312 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) |
2 | 1 | ralbii 2330 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) |
3 | | bnd2.1 |
. . . 4
⊢ 𝐴 ∈ V |
4 | | raleq 2505 |
. . . . 5
⊢ (𝑣 = 𝐴 → (∀𝑥 ∈ 𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) |
5 | | raleq 2505 |
. . . . . 6
⊢ (𝑣 = 𝐴 → (∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) |
6 | 5 | exbidv 1706 |
. . . . 5
⊢ (𝑣 = 𝐴 → (∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) |
7 | 4, 6 | imbi12d 223 |
. . . 4
⊢ (𝑣 = 𝐴 → ((∀𝑥 ∈ 𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)))) |
8 | | bnd 3925 |
. . . 4
⊢
(∀𝑥 ∈
𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) |
9 | 3, 7, 8 | vtocl 2608 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) |
10 | 2, 9 | sylbi 114 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) |
11 | | vex 2560 |
. . . . 5
⊢ 𝑤 ∈ V |
12 | 11 | inex1 3891 |
. . . 4
⊢ (𝑤 ∩ 𝐵) ∈ V |
13 | | inss2 3158 |
. . . . . . 7
⊢ (𝑤 ∩ 𝐵) ⊆ 𝐵 |
14 | | sseq1 2966 |
. . . . . . 7
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (𝑧 ⊆ 𝐵 ↔ (𝑤 ∩ 𝐵) ⊆ 𝐵)) |
15 | 13, 14 | mpbiri 157 |
. . . . . 6
⊢ (𝑧 = (𝑤 ∩ 𝐵) → 𝑧 ⊆ 𝐵) |
16 | 15 | biantrurd 289 |
. . . . 5
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑 ↔ (𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑))) |
17 | | rexeq 2506 |
. . . . . . 7
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ (𝑤 ∩ 𝐵)𝜑)) |
18 | | elin 3126 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑤 ∩ 𝐵) ↔ (𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵)) |
19 | 18 | anbi1i 431 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (𝑤 ∩ 𝐵) ∧ 𝜑) ↔ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
20 | | anass 381 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ↔ (𝑦 ∈ 𝑤 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
21 | 19, 20 | bitri 173 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑤 ∩ 𝐵) ∧ 𝜑) ↔ (𝑦 ∈ 𝑤 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
22 | 21 | rexbii2 2335 |
. . . . . . 7
⊢
(∃𝑦 ∈
(𝑤 ∩ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) |
23 | 17, 22 | syl6bb 185 |
. . . . . 6
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) |
24 | 23 | ralbidv 2326 |
. . . . 5
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) |
25 | 16, 24 | bitr3d 179 |
. . . 4
⊢ (𝑧 = (𝑤 ∩ 𝐵) → ((𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) |
26 | 12, 25 | spcev 2647 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) |
27 | 26 | exlimiv 1489 |
. 2
⊢
(∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) |
28 | 10, 27 | syl 14 |
1
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) |