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 ) ) |
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 ) ) |