Theorem nfrabw 3454

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2108  {cab 2713  Ⅎwnfc 2883  {crab 3415

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-rab 3416

This theorem is referenced by:  nfdifOLD  4105  nfinOLD  4200  nfse  5628  elfvmptrab1w  7012  elovmporab  7651  elovmporab1w  7652  ovmpt3rab1  7663  elovmpt3rab1  7665  mpoxopoveq  8216  nfoi  9526  scottex  9897  elmptrab  23763  iundisjf  32516  nnindf  32744  fedgmullem2  33616  bnj1398  35011  bnj1445  35021  bnj1449  35025  nfwlim  35786  finminlem  36282  poimirlem26  37616  poimirlem27  37617  indexa  37703  nfscott  44211  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  infnsuprnmpt  45222  allbutfiinf  45395  supminfrnmpt  45420  supminfxrrnmpt  45446  fnlimfvre  45651  fnlimabslt  45656  dvnprodlem1  45923  stoweidlem16  45993  stoweidlem31  46008  stoweidlem34  46011  stoweidlem35  46012  stoweidlem48  46025  stoweidlem51  46028  stoweidlem53  46030  stoweidlem54  46031  stoweidlem57  46034  stoweidlem59  46036  fourierdlem31  46115  fourierdlem48  46131  fourierdlem51  46134  etransclem32  46243  ovncvrrp  46541  smflim  46754  smflimmpt  46787  smfsupmpt  46792  smfsupxr  46793  smfinfmpt  46796  smflimsuplem7  46803