Theorem nftpos

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

	Ref	Expression
Hypothesis	nftpos.1	|- F/_ x F
Assertion	nftpos	|- F/_ x tpos F

Proof

Step	Hyp	Ref	Expression
1		nftpos.1	|- F/_ x F
2		dftpos4	|- tpos F = ( F o. ( y e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { y } ) )
3		nfcv	|- F/_ x ( y e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { y } )
4	1 3	nfco	|- F/_ x ( F o. ( y e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { y } ) )
5	2 4	nfcxfr	|- F/_ x tpos F