Metamath Proof Explorer


Definition df-membpart

Description: Define the member partition predicate, or the disjoint restricted element relation on its domain quotient predicate. (Read: A is a member partition.) A alternative definition is dfmembpart2 .

Member partition is the conventional meaning of partition (see the notes of df-parts and dfmembpart2 ), we generalize the concept in df-parts and df-part .

Member partition and comember equivalence are the same by mpet . (Contributed by Peter Mazsa, 26-Jun-2021)

Ref Expression
Assertion df-membpart Could not format assertion : No typesetting found for |- ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 wmembpart Could not format MembPart A : No typesetting found for wff MembPart A with typecode wff
2 cep class E
3 2 ccnv class E -1
4 3 0 cres class E -1 A
5 0 4 wpart Could not format ( `' _E |` A ) Part A : No typesetting found for wff ( `' _E |` A ) Part A with typecode wff
6 1 5 wb Could not format ( MembPart A <-> ( `' _E |` A ) Part A ) : No typesetting found for wff ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode wff