nfrab

Description: A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrabw when possible. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfrab.1	$⊢ Ⅎ x φ$
2		nfrab.2	$⊢ \underline{Ⅎ} x A$
3		df-rab	$⊢ \{y \in A \| φ\} = \{y \| (y \in A \land φ)\}$
4		nftru	$⊢ Ⅎ y ⊤$
5	2	nfcri	$⊢ Ⅎ x z \in A$
6		eleq1w	$⊢ z = y \to (z \in A \leftrightarrow y \in A)$
7	5 6	dvelimnf	$⊢ \neg \forall x x = y \to Ⅎ x y \in A$
8	1	a1i	$⊢ \neg \forall x x = y \to Ⅎ x φ$
9	7 8	nfand	$⊢ \neg \forall x x = y \to Ⅎ x (y \in A \land φ)$
10	9	adantl	$⊢ (⊤ \land \neg \forall x x = y) \to Ⅎ x (y \in A \land φ)$
11	4 10	nfabd2	$⊢ ⊤ \to \underline{Ⅎ} x \{y \| (y \in A \land φ)\}$
12	11	mptru	$⊢ \underline{Ⅎ} x \{y \| (y \in A \land φ)\}$
13	3 12	nfcxfr	$⊢ \underline{Ⅎ} x \{y \in A \| φ\}$

Metamath Proof Explorer

Theorem nfrab

Proof