![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-redunds | Structured version Visualization version GIF version |
Description: Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 37117) is equivalent to satisfying the redundancy predicate (df-redund 37115). (Contributed by Peter Mazsa, 23-Oct-2022.) |
Ref | Expression |
---|---|
df-redunds | ⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | credunds 36683 | . 2 class Redunds | |
2 | vx | . . . . . . 7 setvar 𝑥 | |
3 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
4 | vy | . . . . . . 7 setvar 𝑦 | |
5 | 4 | cv 1541 | . . . . . 6 class 𝑦 |
6 | 3, 5 | wss 3915 | . . . . 5 wff 𝑥 ⊆ 𝑦 |
7 | vz | . . . . . . . 8 setvar 𝑧 | |
8 | 7 | cv 1541 | . . . . . . 7 class 𝑧 |
9 | 3, 8 | cin 3914 | . . . . . 6 class (𝑥 ∩ 𝑧) |
10 | 5, 8 | cin 3914 | . . . . . 6 class (𝑦 ∩ 𝑧) |
11 | 9, 10 | wceq 1542 | . . . . 5 wff (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧) |
12 | 6, 11 | wa 397 | . . . 4 wff (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧)) |
13 | 12, 4, 7, 2 | coprab 7363 | . . 3 class {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
14 | 13 | ccnv 5637 | . 2 class ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
15 | 1, 14 | wceq 1542 | 1 wff Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} |
Colors of variables: wff setvar class |
This definition is referenced by: brredunds 37117 |
Copyright terms: Public domain | W3C validator |