Theorem cpet

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)

	Ref	Expression
Assertion	cpet	$$⊢MembPartA\leftrightarrow \left(EqvRel\sim A\wedge \bigcup A/\sim A=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfmembpart2	$$⊢MembPartA\leftrightarrow \left(ElDisjA\wedge \neg \varnothing \in A\right)$$
2		cpet2	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(EqvRel\sim A\wedge \bigcup A/\sim A=A\right)$$
3	1 2	bitri	$$⊢MembPartA\leftrightarrow \left(EqvRel\sim A\wedge \bigcup A/\sim A=A\right)$$