Theorem nfrab 3325

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 3097	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1767	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrab.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2926	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
5		eleq1w 2848	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
6	4, 5	dvelimnf 2389	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfrab.1	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
8	7	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
9	6, 8	nfand 1860	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
10	9	adantl 474	. . . 4 ⊢ ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
11	2, 10	nfabd2 2953	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
12	11	mptru 1514	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
13	1, 12	nfcxfr 2930	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:  ¬ wn 3   ∧ wa 387  ∀wal 1505  ⊤wtru 1508  Ⅎwnf 1746   ∈ wcel 2050  {cab 2758  Ⅎwnfc 2916  {crab 3092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097

This theorem is referenced by:  nfdif  3992  nfin  4080  nfse  5382  elfvmptrab1  6620  elovmporab  7210  elovmporab1  7211  ovmpt3rab1  7221  elovmpt3rab1  7223  mpoxopoveq  7688  nfoi  8773  scottex  9108  elmptrab  22139  iundisjf  30105  nnindf  30288  fedgmullem2  30661  bnj1398  31957  bnj1445  31967  bnj1449  31971  nfwlim  32636  finminlem  33193  poimirlem26  34365  poimirlem27  34366  indexa  34456  nfscott  39956  binomcxplemdvbinom  40107  binomcxplemdvsum  40109  binomcxplemnotnn0  40110  infnsuprnmpt  40956  allbutfiinf  41131  supminfrnmpt  41156  supminfxrrnmpt  41184  fnlimfvre  41392  fnlimabslt  41397  dvnprodlem1  41667  stoweidlem16  41738  stoweidlem31  41753  stoweidlem34  41756  stoweidlem35  41757  stoweidlem48  41770  stoweidlem51  41773  stoweidlem53  41775  stoweidlem54  41776  stoweidlem57  41779  stoweidlem59  41781  fourierdlem31  41860  fourierdlem48  41876  fourierdlem51  41879  etransclem32  41988  ovncvrrp  42283  smflim  42490  smflimmpt  42521  smfsupmpt  42526  smfsupxr  42527  smfinfmpt  42530  smflimsuplem7  42537