Metamath Proof Explorer

Definition df-membparts

Description: Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021)

Ref Expression
Assertion df-membparts 
|- MembParts = { a | ( `' _E |` a ) Parts a }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmembparts 
 |-  MembParts
1 va 
 |-  a
2 cep 
 |-  _E
3 2 ccnv 
 |-  `' _E
4 1 cv 
 |-  a
5 3 4 cres 
 |-  ( `' _E |` a )
6 cparts 
 |-  Parts
7 5 4 6 wbr 
 |-  ( `' _E |` a ) Parts a
8 7 1 cab 
 |-  { a | ( `' _E |` a ) Parts a }
9 0 8 wceq 
 |-  MembParts = { a | ( `' _E |` a ) Parts a }