Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Domain quotients
dmqseq
Next ⟩
dmqseqi
Metamath Proof Explorer
Ascii
Unicode
Theorem
dmqseq
Description:
Equality theorem for domain quotient.
(Contributed by
Peter Mazsa
, 17-Apr-2019)
Ref
Expression
Assertion
dmqseq
⊢
R
=
S
→
dom
⁡
R
/
R
=
dom
⁡
S
/
S
Proof
Step
Hyp
Ref
Expression
1
dmeq
⊢
R
=
S
→
dom
⁡
R
=
dom
⁡
S
2
qseq12
⊢
dom
⁡
R
=
dom
⁡
S
∧
R
=
S
→
dom
⁡
R
/
R
=
dom
⁡
S
/
S
3
1
2
mpancom
⊢
R
=
S
→
dom
⁡
R
/
R
=
dom
⁡
S
/
S