Theorem nfriota

Description: A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Hypotheses	nfriota.1	|- F/ x ph
	nfriota.2	|- F/_ x A
Assertion	nfriota	|- F/_ x ( iota_ y e. A ph )

Proof

Step	Hyp	Ref	Expression
1		nfriota.1	|- F/ x ph
2		nfriota.2	|- F/_ x A
3		nftru	|- F/ y T.
4	1	a1i	|- ( T. -> F/ x ph )
5	2	a1i	|- ( T. -> F/_ x A )
6	3 4 5	nfriotadw	|- ( T. -> F/_ x ( iota_ y e. A ph ) )
7	6	mptru	|- F/_ x ( iota_ y e. A ph )