Definition df-redunds 38608

Description: Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 38611) is equivalent to satisfying the redundancy predicate (df-redund 38609). (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 38186	. 2 class Redunds
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1539	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1539	. . . . . 6 class 𝑦
6	3, 5	wss 3922	. . . . 5 wff 𝑥 ⊆ 𝑦
7		vz	. . . . . . . 8 setvar 𝑧
8	7	cv 1539	. . . . . . 7 class 𝑧
9	3, 8	cin 3921	. . . . . 6 class (𝑥 ∩ 𝑧)
10	5, 8	cin 3921	. . . . . 6 class (𝑦 ∩ 𝑧)
11	9, 10	wceq 1540	. . . . 5 wff (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧)
12	6, 11	wa 395	. . . 4 wff (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))
13	12, 4, 7, 2	coprab 7395	. . 3 class {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
14	13	ccnv 5645	. 2 class ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
15	1, 14	wceq 1540	1 wff Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}

This definition is referenced by:  brredunds  38611