Metamath Proof Explorer

Theorem dmqseqi

Description: Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021)

Ref Expression
Hypothesis dmqseqi.1 
|- R = S
Assertion dmqseqi 
|- ( dom R /. R ) = ( dom S /. S )

Proof

Step Hyp Ref Expression
1 dmqseqi.1 
 |-  R = S
2 dmqseq 
 |-  ( R = S -> ( dom R /. R ) = ( dom S /. S ) )
3 1 2 ax-mp 
 |-  ( dom R /. R ) = ( dom S /. S )