Theorem nfrabw 3475

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2108  {cab 2714  Ⅎwnfc 2890  {crab 3436

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437

This theorem is referenced by:  nfdifOLD  4130  nfinOLD  4225  nfse  5659  elfvmptrab1w  7043  elovmporab  7679  elovmporab1w  7680  ovmpt3rab1  7691  elovmpt3rab1  7693  mpoxopoveq  8244  nfoi  9554  scottex  9925  elmptrab  23835  iundisjf  32602  nnindf  32821  fedgmullem2  33681  bnj1398  35048  bnj1445  35058  bnj1449  35062  nfwlim  35823  finminlem  36319  poimirlem26  37653  poimirlem27  37654  indexa  37740  nfscott  44258  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  infnsuprnmpt  45257  allbutfiinf  45431  supminfrnmpt  45456  supminfxrrnmpt  45482  fnlimfvre  45689  fnlimabslt  45694  dvnprodlem1  45961  stoweidlem16  46031  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem48  46063  stoweidlem51  46066  stoweidlem53  46068  stoweidlem54  46069  stoweidlem57  46072  stoweidlem59  46074  fourierdlem31  46153  fourierdlem48  46169  fourierdlem51  46172  etransclem32  46281  ovncvrrp  46579  smflim  46792  smflimmpt  46825  smfsupmpt  46830  smfsupxr  46831  smfinfmpt  46834  smflimsuplem7  46841