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	⊢ ( 𝑅 ErALTV 𝐴 → MembPart 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mainer	⊢ ( 𝑅 ErALTV 𝐴 → CoMembEr 𝐴 )
2		mpet	⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴 )
3	1 2	sylibr	⊢ ( 𝑅 ErALTV 𝐴 → MembPart 𝐴 )