Theorem nfoprab3

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

	Ref	Expression
Assertion	nfoprab3	|- F/_ z { <. <. x , y >. , z >. | ph }

Proof

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