Theorem tposex

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

	Ref	Expression
Hypothesis	tposex.1	$$⊢F\in \mathrm{V}$$
Assertion	tposex	$$⊢tposF\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		tposex.1	$$⊢F\in \mathrm{V}$$
2		tposexg	$$⊢F\in \mathrm{V}\to tposF\in \mathrm{V}$$
3	1 2	ax-mp	$$⊢tposF\in \mathrm{V}$$