Theorem nfrabw 3456

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3459 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2365. (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 3419	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1798	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2882	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
6	4, 5	nfan 1894	. . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
7	6	a1i 11	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
8	2, 7	nfabdw 2915	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
9	8	mptru 1540	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
10	1, 9	nfcxfr 2889	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 394  ⊤wtru 1534  Ⅎwnf 1777   ∈ wcel 2098  {cab 2702  Ⅎwnfc 2875  {crab 3418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-rab 3419

This theorem is referenced by:  nfdifOLD  4124  nfinOLD  4217  nfse  5656  elfvmptrab1w  7035  elovmporab  7671  elovmporab1w  7672  ovmpt3rab1  7683  elovmpt3rab1  7685  mpoxopoveq  8233  nfoi  9553  scottex  9924  elmptrab  23814  iundisjf  32500  nnindf  32709  fedgmullem2  33497  bnj1398  34835  bnj1445  34845  bnj1449  34849  nfwlim  35594  finminlem  35978  poimirlem26  37295  poimirlem27  37296  indexa  37382  nfscott  43850  binomcxplemdvbinom  43964  binomcxplemdvsum  43966  binomcxplemnotnn0  43967  infnsuprnmpt  44796  allbutfiinf  44972  supminfrnmpt  44997  supminfxrrnmpt  45023  fnlimfvre  45232  fnlimabslt  45237  dvnprodlem1  45504  stoweidlem16  45574  stoweidlem31  45589  stoweidlem34  45592  stoweidlem35  45593  stoweidlem48  45606  stoweidlem51  45609  stoweidlem53  45611  stoweidlem54  45612  stoweidlem57  45615  stoweidlem59  45617  fourierdlem31  45696  fourierdlem48  45712  fourierdlem51  45715  etransclem32  45824  ovncvrrp  46122  smflim  46335  smflimmpt  46368  smfsupmpt  46373  smfsupxr  46374  smfinfmpt  46377  smflimsuplem7  46384