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

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