Theorem fences3

Description: Implication of eqvrelqseqdisj2 and n0eldmqseq , see comment of fences . (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	fences3	|- ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( ElDisj A /\ -. (/) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj2	|- ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ElDisj A )
2		n0eldmqseq	|- ( ( dom R /. R ) = A -> -. (/) e. A )
3	2	adantl	|- ( ( EqvRel R /\ ( dom R /. R ) = A ) -> -. (/) e. A )
4	1 3	jca	|- ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( ElDisj A /\ -. (/) e. A ) )