Theorem nfopabd

Description: Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Hypotheses	nfopabd.1	|- F/ x ph
	nfopabd.2	|- F/ y ph
	nfopabd.4	|- ( ph -> F/ z ps )
Assertion	nfopabd	|- ( ph -> F/_ z { <. x , y >. | ps } )

Proof

Step	Hyp	Ref	Expression
1		nfopabd.1	|- F/ x ph
2		nfopabd.2	|- F/ y ph
3		nfopabd.4	|- ( ph -> F/ z ps )
4		df-opab	|- { <. x , y >. | ps } = { w | E. x E. y ( w = <. x , y >. /\ ps ) }
5		nfv	|- F/ w ph
6		nfvd	|- ( ph -> F/ z w = <. x , y >. )
7	6 3	nfand	|- ( ph -> F/ z ( w = <. x , y >. /\ ps ) )
8	2 7	nfexd	|- ( ph -> F/ z E. y ( w = <. x , y >. /\ ps ) )
9	1 8	nfexd	|- ( ph -> F/ z E. x E. y ( w = <. x , y >. /\ ps ) )
10	5 9	nfabdw	|- ( ph -> F/_ z { w | E. x E. y ( w = <. x , y >. /\ ps ) } )
11	4 10	nfcxfrd	|- ( ph -> F/_ z { <. x , y >. | ps } )