Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . . . . . . . 10
⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) |
2 | 1 | anim2d 335 |
. . . . . . . . 9
⊢ ((𝜑 → 𝜓) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
3 | 2 | alimi 1435 |
. . . . . . . 8
⊢
(∀𝑧(𝜑 → 𝜓) → ∀𝑧((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
4 | | exim 1579 |
. . . . . . . 8
⊢
(∀𝑧((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)) → (∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
5 | 3, 4 | syl 14 |
. . . . . . 7
⊢
(∀𝑧(𝜑 → 𝜓) → (∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
6 | 5 | alimi 1435 |
. . . . . 6
⊢
(∀𝑦∀𝑧(𝜑 → 𝜓) → ∀𝑦(∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
7 | | exim 1579 |
. . . . . 6
⊢
(∀𝑦(∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)) → (∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
8 | 6, 7 | syl 14 |
. . . . 5
⊢
(∀𝑦∀𝑧(𝜑 → 𝜓) → (∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
9 | 8 | alimi 1435 |
. . . 4
⊢
(∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → ∀𝑥(∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
10 | | exim 1579 |
. . . 4
⊢
(∀𝑥(∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
11 | 9, 10 | syl 14 |
. . 3
⊢
(∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓))) |
12 | 11 | ss2abdv 3201 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ⊆ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)}) |
13 | | df-oprab 5828 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
14 | | df-oprab 5828 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜓} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)} |
15 | 12, 13, 14 | 3sstr4g 3171 |
1
⊢
(∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) |