Theorem nfrabw 3451

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

This proof depends on syntax axioms:   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2147  {cab 2741  Ⅎwnfc 2911  {crab 3416

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417

This theorem is used by:  nfse  5629  elfvmptrab1w  7041  elfvmptrab1  7042  elovmporab  7688  elovmporab1w  7689  elovmporab1  7690  ovmpt3rab1  7700  elovmpt3rab1  7702  mpoxopoveq  8261  nfoi  9532  nfscott  9956  scottexOLD  9958  elmptrab  24173  iundisjf  33252  nnindf  33478  fedgmullem2  34329  bnj1398  35731  bnj1445  35741  bnj1449  35745  rankse  35822  nfwlim  36761  finminlem  37283  poimirlem26  38755  poimirlem27  38756  indexa  38858  binomcxplemdvbinom  45527  binomcxplemdvsum  45529  binomcxplemnotnn0  45530  infnsuprnmpt  46465  allbutfiinf  46633  supminfrnmpt  46658  supminfxrrnmpt  46684  fnlimfvre  46887  fnlimabslt  46892  dvnprodlem1  47159  stoweidlem16  47229  stoweidlem31  47244  stoweidlem34  47247  stoweidlem35  47248  stoweidlem48  47261  stoweidlem51  47264  stoweidlem53  47266  stoweidlem54  47267  stoweidlem57  47270  stoweidlem59  47272  fourierdlem31  47351  fourierdlem48  47367  fourierdlem51  47370  etransclem32  47479  ovncvrrp  47777  smflim  47990  smflimmpt  48023  smfsupmpt  48028  smfsupxr  48029  smfinfmpt  48032  smflimsuplem7  48039