This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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