Theorem nfrabw 3453

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

Syntax hints:   ∧ wa 399  Ⅎwnf 1805   ∈ wcel 2144  {cab 2742  Ⅎwnfc 2911  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-rab 3417

This theorem is referenced by:  nfse  5623  elfvmptrab1w  7005  elovmporab  7644  elovmporab1w  7645  ovmpt3rab1  7656  elovmpt3rab1  7658  mpoxopoveq  8201  nfoi  9464  scottex  9845  elmptrab  23889  iundisjf  32791  nnindf  33024  fedgmullem2  33929  bnj1398  35331  bnj1445  35341  bnj1449  35345  nfwlim  36175  finminlem  36683  poimirlem26  38150  poimirlem27  38151  indexa  38237  nfscott  44820  binomcxplemdvbinom  44934  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  infnsuprnmpt  45830  allbutfiinf  45999  supminfrnmpt  46024  supminfxrrnmpt  46050  fnlimfvre  46253  fnlimabslt  46258  dvnprodlem1  46525  stoweidlem16  46595  stoweidlem31  46610  stoweidlem34  46613  stoweidlem35  46614  stoweidlem48  46627  stoweidlem51  46630  stoweidlem53  46632  stoweidlem54  46633  stoweidlem57  46636  stoweidlem59  46638  fourierdlem31  46717  fourierdlem48  46733  fourierdlem51  46736  etransclem32  46845  ovncvrrp  47143  smflim  47356  smflimmpt  47389  smfsupmpt  47394  smfsupxr  47395  smfinfmpt  47398  smflimsuplem7  47405