Definition df-redund 38625

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

This definition is referenced by:  brredundsredund  38628  redundss3  38629  redundeq1  38630  refrelsredund4  38633