Theorem nfrabw 3427

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

Syntax hints:   ∧ wa 395  Ⅎwnf 1785   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391

This theorem is referenced by:  nfdifOLD  4071  nfinOLD  4166  nfse  5600  elfvmptrab1w  6971  elovmporab  7608  elovmporab1w  7609  ovmpt3rab1  7620  elovmpt3rab1  7622  mpoxopoveq  8164  nfoi  9424  scottex  9804  elmptrab  23806  iundisjf  32678  nnindf  32912  fedgmullem2  33794  bnj1398  35196  bnj1445  35206  bnj1449  35210  nfwlim  36022  finminlem  36520  poimirlem26  37985  poimirlem27  37986  indexa  38072  nfscott  44688  binomcxplemdvbinom  44802  binomcxplemdvsum  44804  binomcxplemnotnn0  44805  infnsuprnmpt  45701  allbutfiinf  45870  supminfrnmpt  45895  supminfxrrnmpt  45921  fnlimfvre  46124  fnlimabslt  46129  dvnprodlem1  46396  stoweidlem16  46466  stoweidlem31  46481  stoweidlem34  46484  stoweidlem35  46485  stoweidlem48  46498  stoweidlem51  46501  stoweidlem53  46503  stoweidlem54  46504  stoweidlem57  46507  stoweidlem59  46509  fourierdlem31  46588  fourierdlem48  46604  fourierdlem51  46607  etransclem32  46716  ovncvrrp  47014  smflim  47227  smflimmpt  47260  smfsupmpt  47265  smfsupxr  47266  smfinfmpt  47269  smflimsuplem7  47276