Theorem nfrabw 3430

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

Syntax hints:   ∧ wa 397  Ⅎwnf 1791   ∈ wcel 2121  {cab 2719  Ⅎwnfc 2888  {crab 3393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-rab 3394

This theorem is referenced by:  nfse  5595  elfvmptrab1w  6967  elovmporab  7606  elovmporab1w  7607  ovmpt3rab1  7618  elovmpt3rab1  7620  mpoxopoveq  8163  nfoi  9423  scottex  9804  elmptrab  23814  iundisjf  32682  nnindf  32916  fedgmullem2  33826  bnj1398  35231  bnj1445  35241  bnj1449  35245  nfwlim  36063  finminlem  36561  poimirlem26  38028  poimirlem27  38029  indexa  38115  nfscott  44698  binomcxplemdvbinom  44812  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  infnsuprnmpt  45708  allbutfiinf  45877  supminfrnmpt  45902  supminfxrrnmpt  45928  fnlimfvre  46131  fnlimabslt  46136  dvnprodlem1  46403  stoweidlem16  46473  stoweidlem31  46488  stoweidlem34  46491  stoweidlem35  46492  stoweidlem48  46505  stoweidlem51  46508  stoweidlem53  46510  stoweidlem54  46511  stoweidlem57  46514  stoweidlem59  46516  fourierdlem31  46595  fourierdlem48  46611  fourierdlem51  46614  etransclem32  46723  ovncvrrp  47021  smflim  47234  smflimmpt  47267  smfsupmpt  47272  smfsupxr  47273  smfinfmpt  47276  smflimsuplem7  47283