Step | Hyp | Ref
| Expression |
1 | | relopabv 5782 |
. . 3
⊢ Rel
{⟨𝑥, 𝑦⟩ ∣ 𝜑} |
2 | | reldif 5776 |
. . 3
⊢ (Rel
{⟨𝑥, 𝑦⟩ ∣ 𝜑} → Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓})) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ Rel
({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) |
4 | | relopabv 5782 |
. 2
⊢ Rel
{⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} |
5 | | sban 2084 |
. . . 4
⊢ ([𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦] ¬ 𝜓) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓)) |
6 | | sban 2084 |
. . . . 5
⊢ ([𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓) ↔ ([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦] ¬ 𝜓)) |
7 | 6 | sbbii 2080 |
. . . 4
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓) ↔ [𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦] ¬ 𝜓)) |
8 | | vopelopabsb 5491 |
. . . . 5
⊢
(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) |
9 | | sbn 2277 |
. . . . . 6
⊢ ([𝑧 / 𝑥] ¬ [𝑤 / 𝑦]𝜓 ↔ ¬ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
10 | | sbn 2277 |
. . . . . . 7
⊢ ([𝑤 / 𝑦] ¬ 𝜓 ↔ ¬ [𝑤 / 𝑦]𝜓) |
11 | 10 | sbbii 2080 |
. . . . . 6
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓 ↔ [𝑧 / 𝑥] ¬ [𝑤 / 𝑦]𝜓) |
12 | | vopelopabsb 5491 |
. . . . . . 7
⊢
(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
13 | 12 | notbii 320 |
. . . . . 6
⊢ (¬
⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ¬ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
14 | 9, 11, 13 | 3bitr4ri 304 |
. . . . 5
⊢ (¬
⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓) |
15 | 8, 14 | anbi12i 628 |
. . . 4
⊢
((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓)) |
16 | 5, 7, 15 | 3bitr4ri 304 |
. . 3
⊢
((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓)) |
17 | | eldif 3925 |
. . 3
⊢
(⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓})) |
18 | | vopelopabsb 5491 |
. . 3
⊢
(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓)) |
19 | 16, 17, 18 | 3bitr4i 303 |
. 2
⊢
(⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}) |
20 | 3, 4, 19 | eqrelriiv 5751 |
1
⊢
({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} |