Detailed syntax breakdown of Definition df-redunds
Step | Hyp | Ref
| Expression |
1 | | credunds 36353 |
. 2
class
Redunds |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑥 |
4 | | vy |
. . . . . . 7
setvar 𝑦 |
5 | 4 | cv 1538 |
. . . . . 6
class 𝑦 |
6 | 3, 5 | wss 3887 |
. . . . 5
wff 𝑥 ⊆ 𝑦 |
7 | | vz |
. . . . . . . 8
setvar 𝑧 |
8 | 7 | cv 1538 |
. . . . . . 7
class 𝑧 |
9 | 3, 8 | cin 3886 |
. . . . . 6
class (𝑥 ∩ 𝑧) |
10 | 5, 8 | cin 3886 |
. . . . . 6
class (𝑦 ∩ 𝑧) |
11 | 9, 10 | wceq 1539 |
. . . . 5
wff (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧) |
12 | 6, 11 | wa 396 |
. . . 4
wff (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧)) |
13 | 12, 4, 7, 2 | coprab 7276 |
. . 3
class
{〈〈𝑦,
𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
14 | 13 | ccnv 5588 |
. 2
class ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
15 | 1, 14 | wceq 1539 |
1
wff Redunds =
◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |