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	⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → ElDisj 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqvreldisj2	⊢ ( EqvRel 𝑅 → ElDisj ( 𝐵 / 𝑅 ) )
2	1	adantr	⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → ElDisj ( 𝐵 / 𝑅 ) )
3		eldisjeq	⊢ ( ( 𝐵 / 𝑅 ) = 𝐴 → ( ElDisj ( 𝐵 / 𝑅 ) ↔ ElDisj 𝐴 ) )
4	3	adantl	⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → ( ElDisj ( 𝐵 / 𝑅 ) ↔ ElDisj 𝐴 ) )
5	2 4	mpbid	⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → ElDisj 𝐴 )