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

Metamath Proof Explorer

Theorem nfrabw

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 13-Oct-2003) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof shortened by Wolf Lammen, 23-Nov-2024)

	Ref	Expression
Hypotheses	nfrabw.1	$⊢ Ⅎ x φ$
	nfrabw.2	$⊢ \underline{Ⅎ} x A$
Assertion	nfrabw	$⊢ \underline{Ⅎ} x \{y \in A \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		nfrabw.1	$⊢ Ⅎ x φ$
2		nfrabw.2	$⊢ \underline{Ⅎ} x A$
3		df-rab	$⊢ \{y \in A \| φ\} = \{y \| (y \in A \land φ)\}$
4		nftru	$⊢ Ⅎ y ⊤$
5	2	nfcri	$⊢ Ⅎ x y \in A$
6	5 1	nfan	$⊢ Ⅎ x (y \in A \land φ)$
7	6	a1i	$⊢ ⊤ \to Ⅎ x (y \in A \land φ)$
8	4 7	nfabdw	$⊢ ⊤ \to \underline{Ⅎ} x \{y \| (y \in A \land φ)\}$
9	8	mptru	$⊢ \underline{Ⅎ} x \{y \| (y \in A \land φ)\}$
10	3 9	nfcxfr	$⊢ \underline{Ⅎ} x \{y \in A \| φ\}$