Metamath Proof Explorer

Theorem qseq12

Description: Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Assertion qseq12 
|- ( ( A = B /\ C = D ) -> ( A /. C ) = ( B /. D ) )

Proof

Step Hyp Ref Expression
1 qseq1 
 |-  ( A = B -> ( A /. C ) = ( B /. C ) )
2 qseq2 
 |-  ( C = D -> ( B /. C ) = ( B /. D ) )
3 1 2 sylan9eq 
 |-  ( ( A = B /\ C = D ) -> ( A /. C ) = ( B /. D ) )