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

Metamath Proof Explorer

Theorem nfsab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016) Remove use of ax-12 . (Revised by SN, 20-Sep-2023)

		Ref	Expression
	Assertion	nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
2		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
3	1 2	nfxfr	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }