Theorem eqvrelqseqdisj2

Description: Implication of eqvreldisj2 , lemma for The Main Theorem of Equivalences mainer . (Contributed by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	eqvrelqseqdisj2	$$⊢\left(EqvRelR\wedge B/R=A\right)\to ElDisjA$$

Proof

Step	Hyp	Ref	Expression
1		eqvreldisj2	$$⊢EqvRelR\to ElDisj\left(B/R\right)$$
2	1	adantr	$$⊢\left(EqvRelR\wedge B/R=A\right)\to ElDisj\left(B/R\right)$$
3		eldisjeq	$$⊢B/R=A\to \left(ElDisj\left(B/R\right)\leftrightarrow ElDisjA\right)$$
4	3	adantl	$$⊢\left(EqvRelR\wedge B/R=A\right)\to \left(ElDisj\left(B/R\right)\leftrightarrow ElDisjA\right)$$
5	2 4	mpbid	$$⊢\left(EqvRelR\wedge B/R=A\right)\to ElDisjA$$