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	$$⊢RErALTVA\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fences	$$⊢RErALTVA\to MembPartA$$
2		dfmembpart2	$$⊢MembPartA\leftrightarrow \left(ElDisjA\wedge \neg \varnothing \in A\right)$$
3	1 2	sylib	$$⊢RErALTVA\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$