Metamath Proof Explorer

Theorem tposeq

Description: Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposeq 
|- ( F = G -> tpos F = tpos G )

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( F = G -> F C_ G )
2 tposss 
 |-  ( F C_ G -> tpos F C_ tpos G )
3 1 2 syl 
 |-  ( F = G -> tpos F C_ tpos G )
4 eqimss2 
 |-  ( F = G -> G C_ F )
5 tposss 
 |-  ( G C_ F -> tpos G C_ tpos F )
6 4 5 syl 
 |-  ( F = G -> tpos G C_ tpos F )
7 3 6 eqssd 
 |-  ( F = G -> tpos F = tpos G )