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=yzx|xyxz=yz-1

Detailed syntax breakdown

Step Hyp Ref Expression
0 credunds classRedunds
1 vy setvary
2 vz setvarz
3 vx setvarx
4 3 cv setvarx
5 1 cv setvary
6 4 5 wss wffxy
7 2 cv setvarz
8 4 7 cin classxz
9 5 7 cin classyz
10 8 9 wceq wffxz=yz
11 6 10 wa wffxyxz=yz
12 11 1 2 3 coprab classyzx|xyxz=yz
13 12 ccnv classyzx|xyxz=yz-1
14 0 13 wceq wffRedunds=yzx|xyxz=yz-1