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

Metamath Proof Explorer

Theorem ressucdifsn2

Description: The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn . (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion ressucdifsn2 ⊢ R ↾ A ∪ A ∖ R ↾ A = R ↾ A

Proof

Step Hyp Ref Expression
1 disjcsn ⊢ A ∩ A = ∅
2 disjresundif ⊢ A ∩ A = ∅ → R ↾ A ∪ A ∖ R ↾ A = R ↾ A
3 1 2 ax-mp ⊢ R ↾ A ∪ A ∖ R ↾ A = R ↾ A