Definition df-redund 36737

Description: Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 36739) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)

Assertion

Ref	Expression
df-redund	⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))

Detailed syntax breakdown of Definition df-redund

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	wredund 36354	. 2 wff 𝐴 Redund ⟨𝐵, 𝐶⟩
5	1, 2	wss 3887	. . 3 wff 𝐴 ⊆ 𝐵
6	1, 3	cin 3886	. . . 4 class (𝐴 ∩ 𝐶)
7	2, 3	cin 3886	. . . 4 class (𝐵 ∩ 𝐶)
8	6, 7	wceq 1539	. . 3 wff (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)
9	5, 8	wa 396	. 2 wff (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
10	4, 9	wb 205	1 wff (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))

This definition is referenced by:  brredundsredund  36740  redundss3  36741  redundeq1  36742  refrelsredund4  36745