Theorem nfoprab

Description: Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013)

	Ref	Expression
Hypothesis	nfoprab.1	$$⊢Ⅎw\phi$$
Assertion	nfoprab	$$⊢\underset{\_}{Ⅎ}w\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfoprab.1	$$⊢Ⅎw\phi$$
2		df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{v|\exists x\exists y\exists z\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
3		nfv	$$⊢Ⅎwv=⟨⟨x,y⟩,z⟩$$
4	3 1	nfan	$$⊢Ⅎw\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
5	4	nfex	$$⊢Ⅎw\exists z\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
6	5	nfex	$$⊢Ⅎw\exists y\exists z\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
7	6	nfex	$$⊢Ⅎw\exists x\exists y\exists z\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}w\left\{v|\exists x\exists y\exists z\left(v=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
9	2 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}w\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$