Theorem nfrabw 3451

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

Hypotheses

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

Assertion

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

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝐴(𝑥, 𝑦)

Proof of Theorem nfrabw

Step	Hyp	Ref	Expression
1		df-rab 3416	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nfrabw.2	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfrabw.1	. . . 4 ⊢ Ⅎ𝑥𝜑
5	3, 4	nfan 1928	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
6	5	nfab 2930	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
7	1, 6	nfcxfr 2922	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 400  Ⅎwnf 1812   ∈ wcel 2142  {cab 2740  Ⅎwnfc 2909  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3416

This theorem is used by:  nfse  5634  elfvmptrab1w  7017  elfvmptrab1  7018  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  ovmpt3rab1  7670  elovmpt3rab1  7672  mpoxopoveq  8213  nfoi  9474  nfscott  9859  scottexOLD  9861  elmptrab  23995  iundisjf  32945  nnindf  33175  fedgmullem2  34029  bnj1398  35431  bnj1445  35441  bnj1449  35445  nfwlim  36320  finminlem  36857  poimirlem26  38325  poimirlem27  38326  indexa  38412  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  infnsuprnmpt  45993  allbutfiinf  46162  supminfrnmpt  46187  supminfxrrnmpt  46213  fnlimfvre  46416  fnlimabslt  46421  dvnprodlem1  46688  stoweidlem16  46758  stoweidlem31  46773  stoweidlem34  46776  stoweidlem35  46777  stoweidlem48  46790  stoweidlem51  46793  stoweidlem53  46795  stoweidlem54  46796  stoweidlem57  46799  stoweidlem59  46801  fourierdlem31  46880  fourierdlem48  46896  fourierdlem51  46899  etransclem32  47008  ovncvrrp  47306  smflim  47519  smflimmpt  47552  smfsupmpt  47557  smfsupxr  47558  smfinfmpt  47561  smflimsuplem7  47568