Metamath Proof Explorer

Theorem tposconst

Description: The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018)

Ref Expression
Assertion tposconst 
|- tpos ( ( A X. B ) X. { C } ) = ( ( B X. A ) X. { C } )

Proof

Step Hyp Ref Expression
1 fconstmpo 
 |-  ( ( A X. B ) X. { C } ) = ( x e. A , y e. B |-> C )
2 1 tposmpo 
 |-  tpos ( ( A X. B ) X. { C } ) = ( y e. B , x e. A |-> C )
3 fconstmpo 
 |-  ( ( B X. A ) X. { C } ) = ( y e. B , x e. A |-> C )
4 2 3 eqtr4i 
 |-  tpos ( ( A X. B ) X. { C } ) = ( ( B X. A ) X. { C } )