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	$$⊢\mathrm{Redunds}={\left\{⟨⟨y,z⟩,x⟩|\left(x\subseteq y\wedge x\cap z=y\cap z\right)\right\}}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		credunds	$$class\mathrm{Redunds}$$
1		vy	$$setvary$$
2		vz	$$setvarz$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	1	cv	$$setvary$$
6	4 5	wss	$$wffx\subseteq y$$
7	2	cv	$$setvarz$$
8	4 7	cin	$$class\left(x\cap z\right)$$
9	5 7	cin	$$class\left(y\cap z\right)$$
10	8 9	wceq	$$wffx\cap z=y\cap z$$
11	6 10	wa	$$wff\left(x\subseteq y\wedge x\cap z=y\cap z\right)$$
12	11 1 2 3	coprab	$$class\left\{⟨⟨y,z⟩,x⟩|\left(x\subseteq y\wedge x\cap z=y\cap z\right)\right\}$$
13	12	ccnv	$$class{\left\{⟨⟨y,z⟩,x⟩|\left(x\subseteq y\wedge x\cap z=y\cap z\right)\right\}}^{-1}$$
14	0 13	wceq	$$wff\mathrm{Redunds}={\left\{⟨⟨y,z⟩,x⟩|\left(x\subseteq y\wedge x\cap z=y\cap z\right)\right\}}^{-1}$$