Metamath Proof Explorer

Theorem fconstmpo

Description: Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018)

Ref Expression
Assertion fconstmpo 
|- ( ( A X. B ) X. { C } ) = ( x e. A , y e. B |-> C )

Proof

Step Hyp Ref Expression
1 fconstmpt 
 |-  ( ( A X. B ) X. { C } ) = ( z e. ( A X. B ) |-> C )
2 eqidd 
 |-  ( z = <. x , y >. -> C = C )
3 2 mpompt 
 |-  ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> C )
4 1 3 eqtri 
 |-  ( ( A X. B ) X. { C } ) = ( x e. A , y e. B |-> C )