Metamath Proof Explorer

Theorem tposex

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

Ref Expression
Hypothesis tposex.1 
|- F e. _V
Assertion tposex 
|- tpos F e. _V

Proof

Step Hyp Ref Expression
1 tposex.1 
 |-  F e. _V
2 tposexg 
 |-  ( F e. _V -> tpos F e. _V )
3 1 2 ax-mp 
 |-  tpos F e. _V