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

Metamath Proof Explorer

Theorem nfrab1

Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997)

		Ref	Expression
	Assertion	nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| φ\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		nfab1	$⊢ \underline{Ⅎ} x \{x \| (x \in A \land φ)\}$
3	1 2	nfcxfr	$⊢ \underline{Ⅎ} x \{x \in A \| φ\}$