This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfmembpart2	⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
2		cpet2	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
3	1 2	bitri	⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )