Theorem nfrabw 3338

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3339 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by NM, 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-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 3115	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1806	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2943	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑦 ∈ 𝐴)
6		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
7	6	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝜑)
8	5, 7	nfand 1898	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
9	2, 8	nfabdw 2976	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
10	9	mptru 1545	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
11	1, 10	nfcxfr 2953	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 399  ⊤wtru 1539  Ⅎwnf 1785   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115

This theorem is referenced by:  nfdif  4053  nfin  4143  nfse  5494  elfvmptrab1w  6771  elovmporab  7371  elovmporab1w  7372  ovmpt3rab1  7383  elovmpt3rab1  7385  mpoxopoveq  7868  nfoi  8962  scottex  9298  elmptrab  22432  iundisjf  30352  nnindf  30561  fedgmullem2  31114  bnj1398  32416  bnj1445  32426  bnj1449  32430  nfwlim  33222  finminlem  33779  poimirlem26  35083  poimirlem27  35084  indexa  35171  nfscott  40947  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  infnsuprnmpt  41888  allbutfiinf  42057  supminfrnmpt  42082  supminfxrrnmpt  42110  fnlimfvre  42316  fnlimabslt  42321  dvnprodlem1  42588  stoweidlem16  42658  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem48  42690  stoweidlem51  42693  stoweidlem53  42695  stoweidlem54  42696  stoweidlem57  42699  stoweidlem59  42701  fourierdlem31  42780  fourierdlem48  42796  fourierdlem51  42799  etransclem32  42908  ovncvrrp  43203  smflim  43410  smflimmpt  43441  smfsupmpt  43446  smfsupxr  43447  smfinfmpt  43450  smflimsuplem7  43457