Theorem nfoprab2

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

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