Theorem nfrabw 3452

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3453 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2404. (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 3417	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nfrabw.2	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2917	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfrabw.1	. . . 4 ⊢ Ⅎ𝑥𝜑
5	3, 4	nfan 1929	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
6	5	nfab 2931	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
7	1, 6	nfcxfr 2923	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 400  Ⅎwnf 1813   ∈ wcel 2143  {cab 2741  Ⅎwnfc 2910  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417

This theorem is used by:  nfse  5635  elfvmptrab1w  7017  elfvmptrab1  7018  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ovmpt3rab1  7668  elovmpt3rab1  7670  mpoxopoveq  8211  nfoi  9472  nfscott  9857  scottexOLD  9859  elmptrab  23993  iundisjf  32943  nnindf  33173  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