Theorem fences2

Description: The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 ) generate a partition of the members, it alo means that ( R ErALTV A -> ElDisj A ) and that ( R ErALTV A -> -. (/) e. A ) . (Contributed by Peter Mazsa, 15-Oct-2021)

	Ref	Expression
Assertion	fences2	|- ( R ErALTV A -> ( ElDisj A /\ -. (/) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		fences	|- ( R ErALTV A -> MembPart A )
2		dfmembpart2	|- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) )
3	1 2	sylib	|- ( R ErALTV A -> ( ElDisj A /\ -. (/) e. A ) )