Definition df-redund 35891

Description: Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 35893) 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 35506	. 2 wff 𝐴 Redund ⟨𝐵, 𝐶⟩
5	1, 2	wss 3924	. . 3 wff 𝐴 ⊆ 𝐵
6	1, 3	cin 3923	. . . 4 class (𝐴 ∩ 𝐶)
7	2, 3	cin 3923	. . . 4 class (𝐵 ∩ 𝐶)
8	6, 7	wceq 1537	. . 3 wff (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)
9	5, 8	wa 398	. 2 wff (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
10	4, 9	wb 208	1 wff (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))

This definition is referenced by:  brredundsredund  35894  redundss3  35895  redundeq1  35896  refrelsredund4  35899