Metamath Proof Explorer

Theorem qseq2i

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

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

Proof

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