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 /\ ( B /. R ) = A ) -> ElDisj A )

Proof

Step Hyp Ref Expression
1 eqvreldisj2 
 |-  ( EqvRel R -> ElDisj ( B /. R ) )
2 1 adantr 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> ElDisj ( B /. R ) )
3 eldisjeq 
 |-  ( ( B /. R ) = A -> ( ElDisj ( B /. R ) <-> ElDisj A ) )
4 3 adantl 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> ( ElDisj ( B /. R ) <-> ElDisj A ) )
5 2 4 mpbid 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> ElDisj A )