Metamath Proof Explorer


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 ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴𝐵 ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) )