Metamath Proof Explorer

Theorem eqvrelqseqdisj5

Description: Lemma for the Partition-Equivalence Theorem pet2 . (Contributed by Peter Mazsa, 15-Jul-2020) (Revised by Peter Mazsa, 22-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj3 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> Disj ( `' _E |` A ) )
2 disjimxrn 
 |-  ( Disj ( `' _E |` A ) -> Disj ( S |X. ( `' _E |` A ) ) )
3 1 2 syl 
 |-  ( ( EqvRel R /\ ( B /. R ) = A ) -> Disj ( S |X. ( `' _E |` A ) ) )