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	⊢ ( 𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fences	⊢ ( 𝑅 ErALTV 𝐴 → MembPart 𝐴 )
2		dfmembpart2	⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
3	1 2	sylib	⊢ ( 𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )