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	Could not format ( R ErALTV A -> MembPart A ) : No typesetting found for |- ( R ErALTV A -> MembPart A ) with typecode |-
2		dfmembpart2	Could not format ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-
3	1 2	sylib	$$⊢RErALTVA\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$