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

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 ∩ E -1 ↾ A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj3 ⊢ EqvRel R ∧ B / R = A → Disj E -1 ↾ A
2 disjimin ⊢ Disj E -1 ↾ A → Disj S ∩ E -1 ↾ A
3 1 2 syl ⊢ EqvRel R ∧ B / R = A → Disj S ∩ E -1 ↾ A