This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 R \land B / R = A) \to ElDisj A$

Step	Hyp	Ref	Expression
1		eqvreldisj2	$⊢ EqvRel R \to ElDisj (B / R)$
2	1	adantr	$⊢ (EqvRel R \land B / R = A) \to ElDisj (B / R)$
3		eldisjeq	$⊢ B / R = A \to (ElDisj (B / R) \leftrightarrow ElDisj A)$
4	3	adantl	$⊢ (EqvRel R \land B / R = A) \to (ElDisj (B / R) \leftrightarrow ElDisj A)$
5	2 4	mpbid	$⊢ (EqvRel R \land B / R = A) \to ElDisj A$