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) (Revised by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Hypothesis	nfopab.1	$$⊢Ⅎz\phi$$
Assertion	nfopab	$$⊢\underset{\_}{Ⅎ}z\left\{⟨x,y⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfopab.1	$$⊢Ⅎz\phi$$
2		nftru	$$⊢Ⅎx\top$$
3		nftru	$$⊢Ⅎy\top$$
4	1	a1i	$$⊢\top \to Ⅎz\phi$$
5	2 3 4	nfopabd	$$⊢\top \to \underset{\_}{Ⅎ}z\left\{⟨x,y⟩|\phi \right\}$$
6	5	mptru	$$⊢\underset{\_}{Ⅎ}z\left\{⟨x,y⟩|\phi \right\}$$