This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tposeq

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

		Ref	Expression
	Assertion	tposeq	$⊢ F = G \to tpos F = tpos G$

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