Definition df-redunds

Description: Define the class of all redundant sets x with respect to y in z . For sets, binary relation on the class of all redundant sets ( brredunds ) is equivalent to satisfying the redundancy predicate ( df-redund ). (Contributed by Peter Mazsa, 23-Oct-2022)

	Ref	Expression
Assertion	df-redunds	|- Redunds = `' { <. <. y , z >. , x >. | ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		credunds	|- Redunds
1		vy	|- y
2		vz	|- z
3		vx	|- x
4	3	cv	|- x
5	1	cv	|- y
6	4 5	wss	|- x C_ y
7	2	cv	|- z
8	4 7	cin	|- ( x i^i z )
9	5 7	cin	|- ( y i^i z )
10	8 9	wceq	|- ( x i^i z ) = ( y i^i z )
11	6 10	wa	|- ( x C_ y /\ ( x i^i z ) = ( y i^i z ) )
12	11 1 2 3	coprab	|- { <. <. y , z >. , x >. | ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) }
13	12	ccnv	|- `' { <. <. y , z >. , x >. | ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) }
14	0 13	wceq	|- Redunds = `' { <. <. y , z >. , x >. | ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) }