Step | Hyp | Ref
| Expression |
1 | | df-in 3873 |
. . 3
⊢ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} |
2 | | df-clab 2715 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓) |
3 | 2 | bicomi 227 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}) |
4 | | df-clab 2715 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒) |
5 | 4 | bicomi 227 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝑦 ∈ {𝑥 ∣ 𝜒}) |
6 | 3, 5 | anbi12i 630 |
. . . . 5
⊢ (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})) |
7 | 6 | abbii 2808 |
. . . 4
⊢ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} |
8 | | sbequ 2089 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
9 | | sbequ 2089 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒)) |
10 | 8, 9 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))) |
11 | 10 | sbievw 2099 |
. . . . . . 7
⊢ ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)) |
12 | | ax-1 6 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)) |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))) |
14 | 13 | impd 414 |
. . . . . . . 8
⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓)) |
15 | | ss2abdv.1 |
. . . . . . . . . 10
⊢ (𝜑 → (𝜓 → 𝜒)) |
16 | 15 | sbimdv 2084 |
. . . . . . . . 9
⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒)) |
17 | 16 | ancld 554 |
. . . . . . . 8
⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))) |
18 | 14, 17 | impbid 215 |
. . . . . . 7
⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓)) |
19 | 11, 18 | syl5bb 286 |
. . . . . 6
⊢ (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓)) |
20 | | df-clab 2715 |
. . . . . 6
⊢ (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)) |
21 | | df-clab 2715 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓) |
22 | 19, 20, 21 | 3bitr4g 317 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥 ∣ 𝜓})) |
23 | 22 | eqrdv 2735 |
. . . 4
⊢ (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥 ∣ 𝜓}) |
24 | 7, 23 | eqtr3id 2792 |
. . 3
⊢ (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} = {𝑥 ∣ 𝜓}) |
25 | 1, 24 | eqtrid 2789 |
. 2
⊢ (𝜑 → ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓}) |
26 | | df-ss 3883 |
. 2
⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓}) |
27 | 25, 26 | sylibr 237 |
1
⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒}) |