Metamath Proof Explorer


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 y x z = y z -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 credunds class Redunds
1 vy setvar y
2 vz setvar z
3 vx setvar x
4 3 cv setvar x
5 1 cv setvar y
6 4 5 wss wff x y
7 2 cv setvar z
8 4 7 cin class x z
9 5 7 cin class y z
10 8 9 wceq wff x z = y z
11 6 10 wa wff x y x z = y z
12 11 1 2 3 coprab class y z x | x y x z = y z
13 12 ccnv class y z x | x y x z = y z -1
14 0 13 wceq wff Redunds = y z x | x y x z = y z -1