Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Partitions: disjoints on domain quotients
parteq2
Next ⟩
parteq12
Metamath Proof Explorer
Ascii
Unicode
Theorem
parteq2
Description:
Equality theorem for partition.
(Contributed by
Peter Mazsa
, 25-Jul-2024)
Ref
Expression
Assertion
parteq2
⊢
A
=
B
→
R
Part
A
↔
R
Part
B
Proof
Step
Hyp
Ref
Expression
1
eqeq2
⊢
A
=
B
→
dom
⁡
R
/
R
=
A
↔
dom
⁡
R
/
R
=
B
2
1
anbi2d
⊢
A
=
B
→
Disj
R
∧
dom
⁡
R
/
R
=
A
↔
Disj
R
∧
dom
⁡
R
/
R
=
B
3
dfpart2
⊢
R
Part
A
↔
Disj
R
∧
dom
⁡
R
/
R
=
A
4
dfpart2
⊢
R
Part
B
↔
Disj
R
∧
dom
⁡
R
/
R
=
B
5
2
3
4
3bitr4g
⊢
A
=
B
→
R
Part
A
↔
R
Part
B