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