Theorem nfoprab3

Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013)

	Ref	Expression
Assertion	nfoprab3	$$⊢\underset{\_}{Ⅎ}z\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	$$⊢Ⅎz\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
3	2	nfex	$$⊢Ⅎz\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
4	3	nfex	$$⊢Ⅎz\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
5	4	nfab	$$⊢\underset{\_}{Ⅎ}z\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
6	1 5	nfcxfr	$$⊢\underset{\_}{Ⅎ}z\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$