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	⊢ Ⅎ 𝑧 𝜑
Assertion	nfopab	⊢ Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfopab.1	⊢ Ⅎ 𝑧 𝜑
2		nftru	⊢ Ⅎ 𝑥 ⊤
3		nftru	⊢ Ⅎ 𝑦 ⊤
4	1	a1i	⊢ ( ⊤ → Ⅎ 𝑧 𝜑 )
5	2 3 4	nfopabd	⊢ ( ⊤ → Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
6	5	mptru	⊢ Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }