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

Metamath Proof Explorer

Theorem partsuc2

Description: Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion partsuc2 ⊢ R ↾ A ∪ A ∖ R ↾ A Part A ∪ A ∖ A ↔ R ↾ A Part A

Proof

Step Hyp Ref Expression
1 ressucdifsn2 ⊢ R ↾ A ∪ A ∖ R ↾ A = R ↾ A
2 sucdifsn2 ⊢ A ∪ A ∖ A = A
3 parteq12 ⊢ R ↾ A ∪ A ∖ R ↾ A = R ↾ A ∧ A ∪ A ∖ A = A → R ↾ A ∪ A ∖ R ↾ A Part A ∪ A ∖ A ↔ R ↾ A Part A
4 1 2 3 mp2an ⊢ R ↾ A ∪ A ∖ R ↾ A Part A ∪ A ∖ A ↔ R ↾ A Part A