Description: The conventional form of Member Partition-Equivalence Theorem. In the
conventional case there is no (general) disjoint and no (general)
partition concept: mathematicians have been calling disjoint or partition
what we call element disjoint or member partition, see also cpet2 . Cf.
mpet , mpet2 and mpet3 for unconventional forms of Member
Partition-Equivalence Theorem. Cf. pet and pet2 for
Partition-Equivalence Theorem with general R . (Contributed by Peter
Mazsa, 31-Dec-2024)
Could not format ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-
Could not format ( MembPart A <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) : No typesetting found for |- ( MembPart A <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) with typecode |-