Metamath Proof Explorer

Theorem disjresundif

Description: Lemma for ressucdifsn2 . (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion disjresundif ⊢ A ∩ B = ∅ → R ↾ A ∪ B ∖ R ↾ B = R ↾ A

Proof

Step Hyp Ref Expression
1 resundi ⊢ R ↾ A ∪ B = R ↾ A ∪ R ↾ B
2 1 difeq1i ⊢ R ↾ A ∪ B ∖ R ↾ B = R ↾ A ∪ R ↾ B ∖ R ↾ B
3 difun2 ⊢ R ↾ A ∪ R ↾ B ∖ R ↾ B = R ↾ A ∖ R ↾ B
4 2 3 eqtri ⊢ R ↾ A ∪ B ∖ R ↾ B = R ↾ A ∖ R ↾ B
5 disjresdif ⊢ A ∩ B = ∅ → R ↾ A ∖ R ↾ B = R ↾ A
6 4 5 eqtrid ⊢ A ∩ B = ∅ → R ↾ A ∪ B ∖ R ↾ B = R ↾ A