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	$$⊢ARedund⟨B,C⟩\leftrightarrow \left(A\subseteq B\wedge A\cap C=B\cap C\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3	0 1 2	wredund	$$wffARedund⟨B,C⟩$$
4	0 1	wss	$$wffA\subseteq B$$
5	0 2	cin	$$class\left(A\cap C\right)$$
6	1 2	cin	$$class\left(B\cap C\right)$$
7	5 6	wceq	$$wffA\cap C=B\cap C$$
8	4 7	wa	$$wff\left(A\subseteq B\wedge A\cap C=B\cap C\right)$$
9	3 8	wb	$$wff\left(ARedund⟨B,C⟩\leftrightarrow \left(A\subseteq B\wedge A\cap C=B\cap C\right)\right)$$