Metamath Proof Explorer


Theorem parteq12

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024)

Ref Expression
Assertion parteq12 R = S A = B R Part A S Part B

Proof

Step Hyp Ref Expression
1 parteq1 R = S R Part A S Part A
2 parteq2 A = B S Part A S Part B
3 1 2 sylan9bb R = S A = B R Part A S Part B