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 ) )