Theorem nfrabw 3385

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3386 with a disjoint variable condition, which does not require ax-13 2390. (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 3147	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1805	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2971	. . . . . 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 3000	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
10	9	mptru 1544	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
11	1, 10	nfcxfr 2975	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 398  ⊤wtru 1538  Ⅎwnf 1784   ∈ wcel 2114  {cab 2799  Ⅎwnfc 2961  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147

This theorem is referenced by:  nfdif  4102  nfin  4193  nfse  5530  elfvmptrab1w  6794  elovmporab  7391  elovmporab1w  7392  ovmpt3rab1  7403  elovmpt3rab1  7405  mpoxopoveq  7885  nfoi  8978  scottex  9314  elmptrab  22435  iundisjf  30339  nnindf  30535  fedgmullem2  31026  bnj1398  32306  bnj1445  32316  bnj1449  32320  nfwlim  33109  finminlem  33666  poimirlem26  34933  poimirlem27  34934  indexa  35023  nfscott  40624  binomcxplemdvbinom  40734  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  infnsuprnmpt  41571  allbutfiinf  41743  supminfrnmpt  41768  supminfxrrnmpt  41796  fnlimfvre  42004  fnlimabslt  42009  dvnprodlem1  42280  stoweidlem16  42350  stoweidlem31  42365  stoweidlem34  42368  stoweidlem35  42369  stoweidlem48  42382  stoweidlem51  42385  stoweidlem53  42387  stoweidlem54  42388  stoweidlem57  42391  stoweidlem59  42393  fourierdlem31  42472  fourierdlem48  42488  fourierdlem51  42491  etransclem32  42600  ovncvrrp  42895  smflim  43102  smflimmpt  43133  smfsupmpt  43138  smfsupxr  43139  smfinfmpt  43142  smflimsuplem7  43149