Theorem nfrabw 3483

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

Syntax hints:   ∧ wa 395  ⊤wtru 1538  Ⅎwnf 1781   ∈ wcel 2108  {cab 2717  Ⅎwnfc 2893  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444

This theorem is referenced by:  nfdifOLD  4153  nfinOLD  4246  nfse  5674  elfvmptrab1w  7056  elovmporab  7696  elovmporab1w  7697  ovmpt3rab1  7708  elovmpt3rab1  7710  mpoxopoveq  8260  nfoi  9583  scottex  9954  elmptrab  23856  iundisjf  32611  nnindf  32823  fedgmullem2  33643  bnj1398  35010  bnj1445  35020  bnj1449  35024  nfwlim  35786  finminlem  36284  poimirlem26  37606  poimirlem27  37607  indexa  37693  nfscott  44208  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  infnsuprnmpt  45159  allbutfiinf  45335  supminfrnmpt  45360  supminfxrrnmpt  45386  fnlimfvre  45595  fnlimabslt  45600  dvnprodlem1  45867  stoweidlem16  45937  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem48  45969  stoweidlem51  45972  stoweidlem53  45974  stoweidlem54  45975  stoweidlem57  45978  stoweidlem59  45980  fourierdlem31  46059  fourierdlem48  46075  fourierdlem51  46078  etransclem32  46187  ovncvrrp  46485  smflim  46698  smflimmpt  46731  smfsupmpt  46736  smfsupxr  46737  smfinfmpt  46740  smflimsuplem7  46747