Theorem tposeq

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

	Ref	Expression
Assertion	tposeq	⊢ ( 𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( 𝐹 = 𝐺 → 𝐹 ⊆ 𝐺 )
2		tposss	⊢ ( 𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺 )
3	1 2	syl	⊢ ( 𝐹 = 𝐺 → tpos 𝐹 ⊆ tpos 𝐺 )
4		eqimss2	⊢ ( 𝐹 = 𝐺 → 𝐺 ⊆ 𝐹 )
5		tposss	⊢ ( 𝐺 ⊆ 𝐹 → tpos 𝐺 ⊆ tpos 𝐹 )
6	4 5	syl	⊢ ( 𝐹 = 𝐺 → tpos 𝐺 ⊆ tpos 𝐹 )
7	3 6	eqssd	⊢ ( 𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺 )