Theorem nfoprab1

Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Assertion	nfoprab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
2		nfe1	$$⊢Ⅎx\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
3	2	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
4	1 3	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$