Metamath Proof Explorer

Theorem qseq1i

Description: Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021)

Ref Expression
Hypothesis qseq1i.1 
|- A = B
Assertion qseq1i 
|- ( A /. C ) = ( B /. C )

Proof

Step Hyp Ref Expression
1 qseq1i.1 
 |-  A = B
2 qseq1 
 |-  ( A = B -> ( A /. C ) = ( B /. C ) )
3 1 2 ax-mp 
 |-  ( A /. C ) = ( B /. C )