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	|- ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2		cC	|- C
3	0 1 2	wredund	|- A Redund <. B , C >.
4	0 1	wss	|- A C_ B
5	0 2	cin	|- ( A i^i C )
6	1 2	cin	|- ( B i^i C )
7	5 6	wceq	|- ( A i^i C ) = ( B i^i C )
8	4 7	wa	|- ( A C_ B /\ ( A i^i C ) = ( B i^i C ) )
9	3 8	wb	|- ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) )