Metamath Proof Explorer

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