Metamath Proof Explorer


Theorem dmqseqeq1i

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

Ref Expression
Hypothesis dmqseqeq1i.1
|- R = S
Assertion dmqseqeq1i
|- ( ( dom R /. R ) = A <-> ( dom S /. S ) = A )

Proof

Step Hyp Ref Expression
1 dmqseqeq1i.1
 |-  R = S
2 dmqseqeq1
 |-  ( R = S -> ( ( dom R /. R ) = A <-> ( dom S /. S ) = A ) )
3 1 2 ax-mp
 |-  ( ( dom R /. R ) = A <-> ( dom S /. S ) = A )