Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Partitions: disjoints on domain quotients
parteq12
Next ⟩
parteq1i
Metamath Proof Explorer
Ascii
Unicode
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