Theorem nfoprab

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

	Ref	Expression
Hypothesis	nfoprab.1	|- F/ w ph
Assertion	nfoprab	|- F/_ w { <. <. x , y >. , z >. | ph }

Proof

Step	Hyp	Ref	Expression
1		nfoprab.1	|- F/ w ph
2		df-oprab	|- { <. <. x , y >. , z >. | ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
3		nfv	|- F/ w v = <. <. x , y >. , z >.
4	3 1	nfan	|- F/ w ( v = <. <. x , y >. , z >. /\ ph )
5	4	nfex	|- F/ w E. z ( v = <. <. x , y >. , z >. /\ ph )
6	5	nfex	|- F/ w E. y E. z ( v = <. <. x , y >. , z >. /\ ph )
7	6	nfex	|- F/ w E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph )
8	7	nfab	|- F/_ w { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
9	2 8	nfcxfr	|- F/_ w { <. <. x , y >. , z >. | ph }