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

Metamath Proof Explorer

Theorem fences

Description: The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet ) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021)

		Ref	Expression
	Assertion	fences	$⊢ R ErALTV A \to MembPart A$

Proof

Step	Hyp	Ref	Expression
1		mainer	$⊢ R ErALTV A \to CoMembEr A$
2		mpet	$⊢ MembPart A \leftrightarrow CoMembEr A$
3	1 2	sylibr	$⊢ R ErALTV A \to MembPart A$