Theorem nfrabw 3472

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3475 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2374. (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 3433	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1800	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrabw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2894	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
5		nfrabw.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
6	4, 5	nfan 1896	. . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
7	6	a1i 11	. . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
8	2, 7	nfabdw 2924	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
9	8	mptru 1543	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
10	1, 9	nfcxfr 2900	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 395  ⊤wtru 1537  Ⅎwnf 1779   ∈ wcel 2105  {cab 2711  Ⅎwnfc 2887  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433

This theorem is referenced by:  nfdifOLD  4139  nfinOLD  4232  nfse  5662  elfvmptrab1w  7042  elovmporab  7678  elovmporab1w  7679  ovmpt3rab1  7690  elovmpt3rab1  7692  mpoxopoveq  8242  nfoi  9551  scottex  9922  elmptrab  23850  iundisjf  32608  nnindf  32825  fedgmullem2  33657  bnj1398  35026  bnj1445  35036  bnj1449  35040  nfwlim  35803  finminlem  36300  poimirlem26  37632  poimirlem27  37633  indexa  37719  nfscott  44234  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  infnsuprnmpt  45194  allbutfiinf  45369  supminfrnmpt  45394  supminfxrrnmpt  45420  fnlimfvre  45629  fnlimabslt  45634  dvnprodlem1  45901  stoweidlem16  45971  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem48  46003  stoweidlem51  46006  stoweidlem53  46008  stoweidlem54  46009  stoweidlem57  46012  stoweidlem59  46014  fourierdlem31  46093  fourierdlem48  46109  fourierdlem51  46112  etransclem32  46221  ovncvrrp  46519  smflim  46732  smflimmpt  46765  smfsupmpt  46770  smfsupxr  46771  smfinfmpt  46774  smflimsuplem7  46781