Definition df-redund

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3	0 1 2	wredund	⊢ 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩
4	0 1	wss	⊢ 𝐴 ⊆ 𝐵
5	0 2	cin	⊢ ( 𝐴 ∩ 𝐶 )
6	1 2	cin	⊢ ( 𝐵 ∩ 𝐶 )
7	5 6	wceq	⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 )
8	4 7	wa	⊢ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) )
9	3 8	wb	⊢ ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )