Theorem tposex

Description: A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Hypothesis	tposex.1	⊢ 𝐹 ∈ V
Assertion	tposex	⊢ tpos 𝐹 ∈ V

Proof

Step	Hyp	Ref	Expression
1		tposex.1	⊢ 𝐹 ∈ V
2		tposexg	⊢ ( 𝐹 ∈ V → tpos 𝐹 ∈ V )
3	1 2	ax-mp	⊢ tpos 𝐹 ∈ V