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 1931	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
6	5	nfab 2928	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
7	1, 6	nfcxfr 2920	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 401  Ⅎwnf 1815   ∈ wcel 2144  {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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413

This theorem is used by:  nfse  5624  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ovmpt3rab1  7679  elovmpt3rab1  7681  mpoxopoveq  8236  nfoi  9508  nfscott  9932  scottexOLD  9934  elmptrab  24146  iundisjf  33183  nnindf  33411  fedgmullem2  34262  bnj1398  35664  bnj1445  35674  bnj1449  35678  nfwlim  36584  finminlem  37106  poimirlem26  38565  poimirlem27  38566  indexa  38668  binomcxplemdvbinom  45337  binomcxplemdvsum  45339  binomcxplemnotnn0  45340  infnsuprnmpt  46262  allbutfiinf  46430  supminfrnmpt  46455  supminfxrrnmpt  46481  fnlimfvre  46684  fnlimabslt  46689  dvnprodlem1  46956  stoweidlem16  47026  stoweidlem31  47041  stoweidlem34  47044  stoweidlem35  47045  stoweidlem48  47058  stoweidlem51  47061  stoweidlem53  47063  stoweidlem54  47064  stoweidlem57  47067  stoweidlem59  47069  fourierdlem31  47148  fourierdlem48  47164  fourierdlem51  47167  etransclem32  47276  ovncvrrp  47574  smflim  47787  smflimmpt  47820  smfsupmpt  47825  smfsupxr  47826  smfinfmpt  47829  smflimsuplem7  47836