Metamath Proof Explorer

Theorem mpteq1OLD

Description: Obsolete version of mpteq1 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mpteq1OLD 
|- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( x e. A -> C = C )
2 1 rgen 
 |-  A. x e. A C = C
3 mpteq12 
 |-  ( ( A = B /\ A. x e. A C = C ) -> ( x e. A |-> C ) = ( x e. B |-> C ) )
4 2 3 mpan2 
 |-  ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )