Theorem nfrabw 3311

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3312 with a disjoint variable condition, which does not require ax-13 2372. (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 3072	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1808	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2893	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑦 ∈ 𝐴)
6		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
7	6	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝜑)
8	5, 7	nfand 1901	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
9	2, 8	nfabdw 2929	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
10	9	mptru 1546	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
11	1, 10	nfcxfr 2904	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 395  ⊤wtru 1540  Ⅎwnf 1787   ∈ wcel 2108  {cab 2715  Ⅎwnfc 2886  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072

This theorem is referenced by:  nfdif  4056  nfin  4147  nfse  5555  elfvmptrab1w  6883  elovmporab  7493  elovmporab1w  7494  ovmpt3rab1  7505  elovmpt3rab1  7507  mpoxopoveq  8006  nfoi  9203  scottex  9574  elmptrab  22886  iundisjf  30829  nnindf  31035  fedgmullem2  31613  bnj1398  32914  bnj1445  32924  bnj1449  32928  nfwlim  33743  finminlem  34434  poimirlem26  35730  poimirlem27  35731  indexa  35818  nfscott  41746  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  infnsuprnmpt  42685  allbutfiinf  42850  supminfrnmpt  42875  supminfxrrnmpt  42901  fnlimfvre  43105  fnlimabslt  43110  dvnprodlem1  43377  stoweidlem16  43447  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem48  43479  stoweidlem51  43482  stoweidlem53  43484  stoweidlem54  43485  stoweidlem57  43488  stoweidlem59  43490  fourierdlem31  43569  fourierdlem48  43585  fourierdlem51  43588  etransclem32  43697  ovncvrrp  43992  smflim  44199  smflimmpt  44230  smfsupmpt  44235  smfsupxr  44236  smfinfmpt  44239  smflimsuplem7  44246