Theorem nfopab2

Description: The second abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 14-Oct-2016)

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

Proof

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