Theorem nfrabw 3434

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

Syntax hints:   ∧ wa 395  ⊤wtru 1542  Ⅎwnf 1784   ∈ wcel 2113  {cab 2712  Ⅎwnfc 2881  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rab 3398

This theorem is referenced by:  nfdifOLD  4080  nfinOLD  4175  nfse  5596  elfvmptrab1w  6966  elovmporab  7602  elovmporab1w  7603  ovmpt3rab1  7614  elovmpt3rab1  7616  mpoxopoveq  8159  nfoi  9417  scottex  9795  elmptrab  23769  iundisjf  32613  nnindf  32849  fedgmullem2  33736  bnj1398  35139  bnj1445  35149  bnj1449  35153  nfwlim  35963  finminlem  36461  poimirlem26  37786  poimirlem27  37787  indexa  37873  nfscott  44422  binomcxplemdvbinom  44536  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  infnsuprnmpt  45436  allbutfiinf  45606  supminfrnmpt  45631  supminfxrrnmpt  45657  fnlimfvre  45860  fnlimabslt  45865  dvnprodlem1  46132  stoweidlem16  46202  stoweidlem31  46217  stoweidlem34  46220  stoweidlem35  46221  stoweidlem48  46234  stoweidlem51  46237  stoweidlem53  46239  stoweidlem54  46240  stoweidlem57  46243  stoweidlem59  46245  fourierdlem31  46324  fourierdlem48  46340  fourierdlem51  46343  etransclem32  46452  ovncvrrp  46750  smflim  46963  smflimmpt  46996  smfsupmpt  47001  smfsupxr  47002  smfinfmpt  47005  smflimsuplem7  47012