Theorem nfopab

Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011)

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

Proof

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