Metamath Proof Explorer

Theorem eqvrelqseqdisj4

Description: Lemma for petincnvepres2 . (Contributed by Peter Mazsa, 31-Dec-2021)

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

Proof

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