Theorem nfrabw 3426

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

Syntax hints:   ∧ wa 395  Ⅎwnf 1785   ∈ wcel 2114  {cab 2714  Ⅎwnfc 2883  {crab 3389

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390

This theorem is referenced by:  nfdifOLD  4070  nfinOLD  4165  nfse  5605  elfvmptrab1w  6975  elovmporab  7613  elovmporab1w  7614  ovmpt3rab1  7625  elovmpt3rab1  7627  mpoxopoveq  8169  nfoi  9429  scottex  9809  elmptrab  23792  iundisjf  32659  nnindf  32893  fedgmullem2  33774  bnj1398  35176  bnj1445  35186  bnj1449  35190  nfwlim  36002  finminlem  36500  poimirlem26  37967  poimirlem27  37968  indexa  38054  nfscott  44666  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  infnsuprnmpt  45679  allbutfiinf  45848  supminfrnmpt  45873  supminfxrrnmpt  45899  fnlimfvre  46102  fnlimabslt  46107  dvnprodlem1  46374  stoweidlem16  46444  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem48  46476  stoweidlem51  46479  stoweidlem53  46481  stoweidlem54  46482  stoweidlem57  46485  stoweidlem59  46487  fourierdlem31  46566  fourierdlem48  46582  fourierdlem51  46585  etransclem32  46694  ovncvrrp  46992  smflim  47205  smflimmpt  47238  smfsupmpt  47243  smfsupxr  47244  smfinfmpt  47247  smflimsuplem7  47254