Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . 6
⊢ 𝑣 ∈ V |
2 | 1 | rabex 4740 |
. . . . 5
⊢ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ∈ V |
3 | | raleq 3115 |
. . . . . . 7
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅)) |
4 | | raleq 3115 |
. . . . . . . 8
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)) |
5 | 4 | raleqbi1dv 3123 |
. . . . . . 7
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)) |
6 | 3, 5 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))) |
7 | | raleq 3115 |
. . . . . . 7
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)) |
8 | 7 | exbidv 1837 |
. . . . . 6
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∃𝑦∀𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)) |
9 | 6, 8 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))) |
10 | 2, 9 | spcv 3272 |
. . . 4
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)) |
11 | 10 | alrimiv 1842 |
. . 3
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)) |
12 | | elrabi 3328 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ∈ 𝑣) |
13 | | elrabi 3328 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑤 ∈ 𝑣) |
14 | 13 | imim1i 61 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑣 → 𝜑) → (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜑)) |
15 | 14 | ralimi2 2933 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝑣 𝜑 → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) |
16 | 12, 15 | imim12i 60 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑣 → ∀𝑤 ∈ 𝑣 𝜑) → (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)) |
17 | 16 | ralimi2 2933 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) |
18 | | neeq1 2844 |
. . . . . . . . 9
⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅)) |
19 | 18 | elrab 3331 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ↔ (𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅)) |
20 | 19 | simprbi 479 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ≠ ∅) |
21 | 20 | rgen 2906 |
. . . . . 6
⊢
∀𝑧 ∈
{𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ |
22 | 17, 21 | jctil 558 |
. . . . 5
⊢
(∀𝑧 ∈
𝑣 ∀𝑤 ∈ 𝑣 𝜑 → (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)) |
23 | 19 | biimpri 217 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}) |
24 | 23 | imim1i 61 |
. . . . . . . 8
⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝜓)) |
25 | 24 | expd 451 |
. . . . . . 7
⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → (𝑧 ∈ 𝑣 → (𝑧 ≠ ∅ → 𝜓))) |
26 | 25 | ralimi2 2933 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) |
27 | 26 | eximi 1752 |
. . . . 5
⊢
(∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) |
28 | 22, 27 | imim12i 60 |
. . . 4
⊢
(((∀𝑧 ∈
{𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))) |
29 | 28 | alimi 1730 |
. . 3
⊢
(∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))) |
30 | 11, 29 | syl 17 |
. 2
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))) |
31 | | raleq 3115 |
. . . . 5
⊢ (𝑣 = 𝑥 → (∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑤 ∈ 𝑥 𝜑)) |
32 | 31 | raleqbi1dv 3123 |
. . . 4
⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑)) |
33 | | raleq 3115 |
. . . . 5
⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))) |
34 | 33 | exbidv 1837 |
. . . 4
⊢ (𝑣 = 𝑥 → (∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))) |
35 | 32, 34 | imbi12d 333 |
. . 3
⊢ (𝑣 = 𝑥 → ((∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))) |
36 | 35 | cbvalv 2261 |
. 2
⊢
(∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))) |
37 | 30, 36 | sylib 207 |
1
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))) |