Theorem nfrabw 3438

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3440 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 3402	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1806	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2891	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
6	4, 5	nfan 1901	. . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
7	6	a1i 11	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
8	2, 7	nfabdw 2921	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
9	8	mptru 1549	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
10	1, 9	nfcxfr 2897	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 395  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3401

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 3402

This theorem is referenced by:  nfdifOLD  4084  nfinOLD  4179  nfse  5608  elfvmptrab1w  6979  elovmporab  7616  elovmporab1w  7617  ovmpt3rab1  7628  elovmpt3rab1  7630  mpoxopoveq  8173  nfoi  9433  scottex  9811  elmptrab  23788  iundisjf  32682  nnindf  32917  fedgmullem2  33814  bnj1398  35216  bnj1445  35226  bnj1449  35230  nfwlim  36042  finminlem  36540  poimirlem26  37926  poimirlem27  37927  indexa  38013  nfscott  44624  binomcxplemdvbinom  44738  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  infnsuprnmpt  45637  allbutfiinf  45807  supminfrnmpt  45832  supminfxrrnmpt  45858  fnlimfvre  46061  fnlimabslt  46066  dvnprodlem1  46333  stoweidlem16  46403  stoweidlem31  46418  stoweidlem34  46421  stoweidlem35  46422  stoweidlem48  46435  stoweidlem51  46438  stoweidlem53  46440  stoweidlem54  46441  stoweidlem57  46444  stoweidlem59  46446  fourierdlem31  46525  fourierdlem48  46541  fourierdlem51  46544  etransclem32  46653  ovncvrrp  46951  smflim  47164  smflimmpt  47197  smfsupmpt  47202  smfsupxr  47203  smfinfmpt  47206  smflimsuplem7  47213