Theorem nfrabw 3460

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3461 with a disjoint variable condition, which does not require ax-13 2410. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2410. (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 3424	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nfrabw.2	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfrabw.1	. . . 4 ⊢ Ⅎ𝑥𝜑
5	3, 4	nfan 1926	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
6	5	nfab 2937	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
7	1, 6	nfcxfr 2929	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 400  Ⅎwnf 1810   ∈ wcel 2149  {cab 2747  Ⅎwnfc 2916  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rab 3424

This theorem is referenced by:  nfse  5636  elfvmptrab1w  7018  elovmporab  7657  elovmporab1w  7658  ovmpt3rab1  7669  elovmpt3rab1  7671  mpoxopoveq  8215  nfoi  9476  scottex  9859  nfscott  9865  elmptrab  23953  iundisjf  32875  nnindf  33105  fedgmullem2  33965  bnj1398  35367  bnj1445  35377  bnj1449  35381  nfwlim  36245  finminlem  36752  poimirlem26  38219  poimirlem27  38220  indexa  38306  binomcxplemdvbinom  44989  binomcxplemdvsum  44991  binomcxplemnotnn0  44992  infnsuprnmpt  45891  allbutfiinf  46060  supminfrnmpt  46085  supminfxrrnmpt  46111  fnlimfvre  46314  fnlimabslt  46319  dvnprodlem1  46586  stoweidlem16  46656  stoweidlem31  46671  stoweidlem34  46674  stoweidlem35  46675  stoweidlem48  46688  stoweidlem51  46691  stoweidlem53  46693  stoweidlem54  46694  stoweidlem57  46697  stoweidlem59  46699  fourierdlem31  46778  fourierdlem48  46794  fourierdlem51  46797  etransclem32  46906  ovncvrrp  47204  smflim  47417  smflimmpt  47450  smfsupmpt  47455  smfsupxr  47456  smfinfmpt  47459  smflimsuplem7  47466