| Step | Hyp | Ref
 | Expression | 
| 1 |   | df-rex 2481 | 
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 2 | 1 | ralbii 2503 | 
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 3 |   | bnd2.1 | 
. . . 4
⊢ 𝐴 ∈ V | 
| 4 |   | raleq 2693 | 
. . . . 5
⊢ (𝑣 = 𝐴 → (∀𝑥 ∈ 𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 5 |   | raleq 2693 | 
. . . . . 6
⊢ (𝑣 = 𝐴 → (∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 6 | 5 | exbidv 1839 | 
. . . . 5
⊢ (𝑣 = 𝐴 → (∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 7 | 4, 6 | imbi12d 234 | 
. . . 4
⊢ (𝑣 = 𝐴 → ((∀𝑥 ∈ 𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)))) | 
| 8 |   | bnd 4205 | 
. . . 4
⊢
(∀𝑥 ∈
𝑣 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝑣 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 9 | 3, 7, 8 | vtocl 2818 | 
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 10 | 2, 9 | sylbi 121 | 
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 11 |   | vex 2766 | 
. . . . 5
⊢ 𝑤 ∈ V | 
| 12 | 11 | inex1 4167 | 
. . . 4
⊢ (𝑤 ∩ 𝐵) ∈ V | 
| 13 |   | inss2 3384 | 
. . . . . . 7
⊢ (𝑤 ∩ 𝐵) ⊆ 𝐵 | 
| 14 |   | sseq1 3206 | 
. . . . . . 7
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (𝑧 ⊆ 𝐵 ↔ (𝑤 ∩ 𝐵) ⊆ 𝐵)) | 
| 15 | 13, 14 | mpbiri 168 | 
. . . . . 6
⊢ (𝑧 = (𝑤 ∩ 𝐵) → 𝑧 ⊆ 𝐵) | 
| 16 | 15 | biantrurd 305 | 
. . . . 5
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑 ↔ (𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑))) | 
| 17 |   | rexeq 2694 | 
. . . . . . 7
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ (𝑤 ∩ 𝐵)𝜑)) | 
| 18 |   | elin 3346 | 
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑤 ∩ 𝐵) ↔ (𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵)) | 
| 19 | 18 | anbi1i 458 | 
. . . . . . . . 9
⊢ ((𝑦 ∈ (𝑤 ∩ 𝐵) ∧ 𝜑) ↔ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | 
| 20 |   | anass 401 | 
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ↔ (𝑦 ∈ 𝑤 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 21 | 19, 20 | bitri 184 | 
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑤 ∩ 𝐵) ∧ 𝜑) ↔ (𝑦 ∈ 𝑤 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 22 | 21 | rexbii2 2508 | 
. . . . . . 7
⊢
(∃𝑦 ∈
(𝑤 ∩ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑)) | 
| 23 | 17, 22 | bitrdi 196 | 
. . . . . 6
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 24 | 23 | ralbidv 2497 | 
. . . . 5
⊢ (𝑧 = (𝑤 ∩ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 25 | 16, 24 | bitr3d 190 | 
. . . 4
⊢ (𝑧 = (𝑤 ∩ 𝐵) → ((𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑))) | 
| 26 | 12, 25 | spcev 2859 | 
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) | 
| 27 | 26 | exlimiv 1612 | 
. 2
⊢
(∃𝑤∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑤 (𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) | 
| 28 | 10, 27 | syl 14 | 
1
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) |