Theorem tposf

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

	Ref	Expression
Assertion	tposf	|- ( F : ( A X. B ) --> C -> tpos F : ( B X. A ) --> C )

Proof

Step	Hyp	Ref	Expression
1		relxp	|- Rel ( A X. B )
2		tposf2	|- ( Rel ( A X. B ) -> ( F : ( A X. B ) --> C -> tpos F : `' ( A X. B ) --> C ) )
3	1 2	ax-mp	|- ( F : ( A X. B ) --> C -> tpos F : `' ( A X. B ) --> C )
4		cnvxp	|- `' ( A X. B ) = ( B X. A )
5	4	feq2i	|- ( tpos F : `' ( A X. B ) --> C <-> tpos F : ( B X. A ) --> C )
6	3 5	sylib	|- ( F : ( A X. B ) --> C -> tpos F : ( B X. A ) --> C )