Theorem nfriota1

Description: The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Assertion	nfriota1	$$⊢\underset{\_}{Ⅎ}x\left(\iota x\in A|\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-riota	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
2		nfiota1	$$⊢\underset{\_}{Ⅎ}x\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
3	1 2	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(\iota x\in A|\phi \right)$$