Theorem nfrabw 3432

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  {crab 3394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3395

This theorem is referenced by:  nfdifOLD  4081  nfinOLD  4176  nfse  5593  elfvmptrab1w  6957  elovmporab  7595  elovmporab1w  7596  ovmpt3rab1  7607  elovmpt3rab1  7609  mpoxopoveq  8152  nfoi  9406  scottex  9781  elmptrab  23712  iundisjf  32533  nnindf  32765  fedgmullem2  33603  bnj1398  35007  bnj1445  35017  bnj1449  35021  nfwlim  35806  finminlem  36302  poimirlem26  37636  poimirlem27  37637  indexa  37723  nfscott  44222  binomcxplemdvbinom  44336  binomcxplemdvsum  44338  binomcxplemnotnn0  44339  infnsuprnmpt  45238  allbutfiinf  45409  supminfrnmpt  45434  supminfxrrnmpt  45460  fnlimfvre  45665  fnlimabslt  45670  dvnprodlem1  45937  stoweidlem16  46007  stoweidlem31  46022  stoweidlem34  46025  stoweidlem35  46026  stoweidlem48  46039  stoweidlem51  46042  stoweidlem53  46044  stoweidlem54  46045  stoweidlem57  46048  stoweidlem59  46050  fourierdlem31  46129  fourierdlem48  46145  fourierdlem51  46148  etransclem32  46257  ovncvrrp  46555  smflim  46768  smflimmpt  46801  smfsupmpt  46806  smfsupxr  46807  smfinfmpt  46810  smflimsuplem7  46817