Metamath Proof Explorer

Theorem eqvrelqseqdisj3

Description: Implication of eqvreldisj3 , lemma for the Member Partition Equivalence Theorem mpet3 . (Contributed by Peter Mazsa, 27-Oct-2020) (Revised by Peter Mazsa, 24-Sep-2021)

Ref Expression
Assertion eqvrelqseqdisj3 
|- ( ( EqvRel R /\ ( B /. R ) = A ) -> Disj ( `' _E |` A ) )

Proof

Step Hyp Ref Expression
1 eqvreldisj3 
 |-  ( EqvRel R -> Disj ( `' _E |` ( B /. R ) ) )
2 1 adantr 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> Disj ( `' _E |` ( B /. R ) ) )
3 reseq2 
 |-  ( ( B /. R ) = A -> ( `' _E |` ( B /. R ) ) = ( `' _E |` A ) )
4 3 disjeqd 
 |-  ( ( B /. R ) = A -> ( Disj ( `' _E |` ( B /. R ) ) <-> Disj ( `' _E |` A ) ) )
5 4 adantl 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> ( Disj ( `' _E |` ( B /. R ) ) <-> Disj ( `' _E |` A ) ) )
6 2 5 mpbid 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> Disj ( `' _E |` A ) )