Theorem nfopabd

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

	Ref	Expression
Hypotheses	nfopabd.1	$$⊢Ⅎx\phi$$
	nfopabd.2	$$⊢Ⅎy\phi$$
	nfopabd.4	$$⊢\phi \to Ⅎz\psi$$
Assertion	nfopabd	$$⊢\phi \to \underset{\_}{Ⅎ}z\left\{⟨x,y⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfopabd.1	$$⊢Ⅎx\phi$$
2		nfopabd.2	$$⊢Ⅎy\phi$$
3		nfopabd.4	$$⊢\phi \to Ⅎz\psi$$
4		df-opab	$$⊢\left\{⟨x,y⟩|\psi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \psi \right)\right\}$$
5		nfv	$$⊢Ⅎw\phi$$
6		nfvd	$$⊢\phi \to Ⅎzw=⟨x,y⟩$$
7	6 3	nfand	$$⊢\phi \to Ⅎz\left(w=⟨x,y⟩\wedge \psi \right)$$
8	2 7	nfexd	$$⊢\phi \to Ⅎz\exists y\left(w=⟨x,y⟩\wedge \psi \right)$$
9	1 8	nfexd	$$⊢\phi \to Ⅎz\exists x\exists y\left(w=⟨x,y⟩\wedge \psi \right)$$
10	5 9	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}z\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \psi \right)\right\}$$
11	4 10	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}z\left\{⟨x,y⟩|\psi \right\}$$