Theorem nfrabw 3447

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

This proof depends on syntax axioms:   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2145  {cab 2738  Ⅎwnfc 2907  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413

This theorem is used by:  nfse  5629  elfvmptrab1w  7017  elfvmptrab1  7018  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  ovmpt3rab1  7675  elovmpt3rab1  7677  mpoxopoveq  8222  nfoi  9493  nfscott  9896  scottexOLD  9898  elmptrab  24085  iundisjf  33094  nnindf  33322  fedgmullem2  34173  bnj1398  35576  bnj1445  35586  bnj1449  35590  nfwlim  36482  finminlem  37004  poimirlem26  38460  poimirlem27  38461  indexa  38548  binomcxplemdvbinom  45242  binomcxplemdvsum  45244  binomcxplemnotnn0  45245  infnsuprnmpt  46144  allbutfiinf  46313  supminfrnmpt  46338  supminfxrrnmpt  46364  fnlimfvre  46567  fnlimabslt  46572  dvnprodlem1  46839  stoweidlem16  46909  stoweidlem31  46924  stoweidlem34  46927  stoweidlem35  46928  stoweidlem48  46941  stoweidlem51  46944  stoweidlem53  46946  stoweidlem54  46947  stoweidlem57  46950  stoweidlem59  46952  fourierdlem31  47031  fourierdlem48  47047  fourierdlem51  47050  etransclem32  47159  ovncvrrp  47457  smflim  47670  smflimmpt  47703  smfsupmpt  47708  smfsupxr  47709  smfinfmpt  47712  smflimsuplem7  47719