Metamath Proof Explorer

Theorem bj-projeq2

Description: Substitution property for Proj . (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-projeq2 
|- ( B = C -> ( A Proj B ) = ( A Proj C ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 bj-projeq 
 |-  ( A = A -> ( B = C -> ( A Proj B ) = ( A Proj C ) ) )
3 1 2 ax-mp 
 |-  ( B = C -> ( A Proj B ) = ( A Proj C ) )