Metamath Proof Explorer

Theorem tposfn

Description: Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion tposfn 
|- ( F Fn ( A X. B ) -> tpos F Fn ( B X. A ) )

Proof

Step Hyp Ref Expression
1 tposf 
 |-  ( F : ( A X. B ) --> _V -> tpos F : ( B X. A ) --> _V )
2 dffn2 
 |-  ( F Fn ( A X. B ) <-> F : ( A X. B ) --> _V )
3 dffn2 
 |-  ( tpos F Fn ( B X. A ) <-> tpos F : ( B X. A ) --> _V )
4 1 2 3 3imtr4i 
 |-  ( F Fn ( A X. B ) -> tpos F Fn ( B X. A ) )