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