Theorem tposeq

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

	Ref	Expression
Assertion	tposeq	$$⊢F=G\to tposF=tposG$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢F=G\to F\subseteq G$$
2		tposss	$$⊢F\subseteq G\to tposF\subseteq tposG$$
3	1 2	syl	$$⊢F=G\to tposF\subseteq tposG$$
4		eqimss2	$$⊢F=G\to G\subseteq F$$
5		tposss	$$⊢G\subseteq F\to tposG\subseteq tposF$$
6	4 5	syl	$$⊢F=G\to tposG\subseteq tposF$$
7	3 6	eqssd	$$⊢F=G\to tposF=tposG$$