Theorem nfrabw 3437

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 2371. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2371. (Revised by Gino Giotto, 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 3405	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1806	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2892	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
6	4, 5	nfan 1902	. . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
7	6	a1i 11	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
8	2, 7	nfabdw 2928	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
9	8	mptru 1548	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
10	1, 9	nfcxfr 2903	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 397  ⊤wtru 1542  Ⅎwnf 1785   ∈ wcel 2106  {cab 2714  Ⅎwnfc 2885  {crab 3404

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-rab 3405

This theorem is referenced by:  nfdif  4077  nfin  4168  nfse  5600  elfvmptrab1w  6962  elovmporab  7582  elovmporab1w  7583  ovmpt3rab1  7594  elovmpt3rab1  7596  mpoxopoveq  8110  nfoi  9376  scottex  9747  elmptrab  23084  iundisjf  31213  nnindf  31418  fedgmullem2  32007  bnj1398  33311  bnj1445  33321  bnj1449  33325  nfwlim  34095  finminlem  34644  poimirlem26  35957  poimirlem27  35958  indexa  36045  nfscott  42228  binomcxplemdvbinom  42342  binomcxplemdvsum  42344  binomcxplemnotnn0  42345  infnsuprnmpt  43174  allbutfiinf  43345  supminfrnmpt  43370  supminfxrrnmpt  43396  fnlimfvre  43601  fnlimabslt  43606  dvnprodlem1  43873  stoweidlem16  43943  stoweidlem31  43958  stoweidlem34  43961  stoweidlem35  43962  stoweidlem48  43975  stoweidlem51  43978  stoweidlem53  43980  stoweidlem54  43981  stoweidlem57  43984  stoweidlem59  43986  fourierdlem31  44065  fourierdlem48  44081  fourierdlem51  44084  etransclem32  44193  ovncvrrp  44489  smflim  44702  smflimmpt  44735  smfsupmpt  44740  smfsupxr  44741  smfinfmpt  44744  smflimsuplem7  44751