Definition df-redunds 35901

Description: Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 35904) is equivalent to satisfying the redundancy predicate (df-redund 35902). (Contributed by Peter Mazsa, 23-Oct-2022.)

Assertion

Ref	Expression
df-redunds	⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-redunds

Step	Hyp	Ref	Expression
1		credunds 35516	. 2 class Redunds
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1535	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1535	. . . . . 6 class 𝑦
6	3, 5	wss 3929	. . . . 5 wff 𝑥 ⊆ 𝑦
7		vz	. . . . . . . 8 setvar 𝑧
8	7	cv 1535	. . . . . . 7 class 𝑧
9	3, 8	cin 3928	. . . . . 6 class (𝑥 ∩ 𝑧)
10	5, 8	cin 3928	. . . . . 6 class (𝑦 ∩ 𝑧)
11	9, 10	wceq 1536	. . . . 5 wff (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧)
12	6, 11	wa 398	. . . 4 wff (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))
13	12, 4, 7, 2	coprab 7150	. . 3 class {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
14	13	ccnv 5547	. 2 class ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
15	1, 14	wceq 1536	1 wff Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}

This definition is referenced by:  brredunds  35904