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	$$⊢Ⅎx\phi$$
	nfriota.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfriota	$$⊢\underset{\_}{Ⅎ}x\left(\iota y\in A|\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfriota.1	$$⊢Ⅎx\phi$$
2		nfriota.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nftru	$$⊢Ⅎy\top$$
4	1	a1i	$$⊢\top \to Ⅎx\phi$$
5	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
6	3 4 5	nfriotadw	$$⊢\top \to \underset{\_}{Ⅎ}x\left(\iota y\in A|\phi \right)$$
7	6	mptru	$$⊢\underset{\_}{Ⅎ}x\left(\iota y\in A|\phi \right)$$