Theorem nfrab 3100

Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

Ref	Expression
nfrab.1	⊢ Ⅎ𝑥𝜑
nfrab.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfrab	⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Proof of Theorem nfrab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 2905	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1721	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrab.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2745	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
5		eleq1 2676	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
6	4, 5	dvelimnf 2327	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfrab.1	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
8	7	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
9	6, 8	nfand 1814	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
10	9	adantl 481	. . . 4 ⊢ ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
11	2, 10	nfabd2 2770	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
12	11	trud 1484	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
13	1, 12	nfcxfr 2749	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:  ¬ wn 3   ∧ wa 383  ∀wal 1473  ⊤wtru 1476  Ⅎwnf 1699   ∈ wcel 1977  {cab 2596  Ⅎwnfc 2738  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905

This theorem is referenced by:  nfdif  3693  nfin  3782  nfse  5013  elfvmptrab1  6213  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rab1  6789  elovmpt3rab1  6791  mpt2xopoveq  7232  nfoi  8302  scottex  8631  elmptrab  21440  iundisjf  28784  nnindf  28952  bnj1398  30356  bnj1445  30366  bnj1449  30370  nfwlim  31012  finminlem  31482  poimirlem26  32605  poimirlem27  32606  indexa  32698  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  fnlimfvre  38741  fnlimabslt  38746  dvnprodlem1  38836  stoweidlem16  38909  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem48  38941  stoweidlem51  38944  stoweidlem53  38946  stoweidlem54  38947  stoweidlem57  38950  stoweidlem59  38952  fourierdlem31  39031  fourierdlem48  39047  fourierdlem51  39050  etransclem32  39159  ovncvrrp  39454  smflim  39663