Theorem nfrabw 3440

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3442 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 3403	. 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 3402

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 3403

This theorem is referenced by:  nfdifOLD  4089  nfinOLD  4184  nfse  5605  elfvmptrab1w  6977  elovmporab  7615  elovmporab1w  7616  ovmpt3rab1  7627  elovmpt3rab1  7629  mpoxopoveq  8175  nfoi  9443  scottex  9814  elmptrab  23747  iundisjf  32568  nnindf  32794  fedgmullem2  33619  bnj1398  35017  bnj1445  35027  bnj1449  35031  nfwlim  35803  finminlem  36299  poimirlem26  37633  poimirlem27  37634  indexa  37720  nfscott  44221  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  infnsuprnmpt  45237  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