Step | Hyp | Ref
| Expression |
1 | | ssintab 4855 |
. . . 4
⊢ (𝐴 ⊆ ∩ {𝑥
∣ 𝜑} ↔
∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) |
2 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝜑) |
3 | | ancr 550 |
. . . . . . . 8
⊢ ((𝜑 → 𝐴 ⊆ 𝑥) → (𝜑 → (𝐴 ⊆ 𝑥 ∧ 𝜑))) |
4 | 2, 3 | impbid2 229 |
. . . . . . 7
⊢ ((𝜑 → 𝐴 ⊆ 𝑥) → ((𝐴 ⊆ 𝑥 ∧ 𝜑) ↔ 𝜑)) |
5 | 4 | imbi1d 345 |
. . . . . 6
⊢ ((𝜑 → 𝐴 ⊆ 𝑥) → (((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ (𝜑 → 𝑦 ∈ 𝑥))) |
6 | 5 | alimi 1813 |
. . . . 5
⊢
(∀𝑥(𝜑 → 𝐴 ⊆ 𝑥) → ∀𝑥(((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ (𝜑 → 𝑦 ∈ 𝑥))) |
7 | | albi 1820 |
. . . . 5
⊢
(∀𝑥(((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ (𝜑 → 𝑦 ∈ 𝑥)) → (∀𝑥((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ ∀𝑥(𝜑 → 𝑦 ∈ 𝑥))) |
8 | 6, 7 | syl 17 |
. . . 4
⊢
(∀𝑥(𝜑 → 𝐴 ⊆ 𝑥) → (∀𝑥((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ ∀𝑥(𝜑 → 𝑦 ∈ 𝑥))) |
9 | 1, 8 | sylbi 220 |
. . 3
⊢ (𝐴 ⊆ ∩ {𝑥
∣ 𝜑} →
(∀𝑥((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥) ↔ ∀𝑥(𝜑 → 𝑦 ∈ 𝑥))) |
10 | | vex 3444 |
. . . 4
⊢ 𝑦 ∈ V |
11 | 10 | elintab 4849 |
. . 3
⊢ (𝑦 ∈ ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} ↔ ∀𝑥((𝐴 ⊆ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑥)) |
12 | 10 | elintab 4849 |
. . 3
⊢ (𝑦 ∈ ∩ {𝑥
∣ 𝜑} ↔
∀𝑥(𝜑 → 𝑦 ∈ 𝑥)) |
13 | 9, 11, 12 | 3bitr4g 317 |
. 2
⊢ (𝐴 ⊆ ∩ {𝑥
∣ 𝜑} → (𝑦 ∈ ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} ↔ 𝑦 ∈ ∩ {𝑥 ∣ 𝜑})) |
14 | 13 | eqrdv 2796 |
1
⊢ (𝐴 ⊆ ∩ {𝑥
∣ 𝜑} → ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) |