Metamath Proof Explorer


Theorem parteq1

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion parteq1 R = S R Part A S Part A

Proof

Step Hyp Ref Expression
1 disjdmqseqeq1 R = S Disj R dom R / R = A Disj S dom S / S = A
2 dfpart2 R Part A Disj R dom R / R = A
3 dfpart2 S Part A Disj S dom S / S = A
4 1 2 3 3bitr4g R = S R Part A S Part A