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

Metamath Proof Explorer

Theorem nfab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016)

		Ref	Expression
	Assertion	nfab1	$⊢ \underline{Ⅎ} x \{x \| φ\}$

Step	Hyp	Ref	Expression
1		nfsab1	$⊢ Ⅎ x y \in \{x \| φ\}$
2	1	nfci	$⊢ \underline{Ⅎ} x \{x \| φ\}$