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