Metamath Proof Explorer


Theorem parteq1d

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

Ref Expression
Hypothesis parteq1d.1 φ R = S
Assertion parteq1d φ R Part A S Part A

Proof

Step Hyp Ref Expression
1 parteq1d.1 φ R = S
2 parteq1 R = S R Part A S Part A
3 1 2 syl φ R Part A S Part A