Theorem nfrabw 3432

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

Syntax hints:   ∧ wa 395  ⊤wtru 1542  Ⅎwnf 1784   ∈ wcel 2111  {cab 2709  Ⅎwnfc 2879  {crab 3395

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rab 3396

This theorem is referenced by:  nfdifOLD  4077  nfinOLD  4172  nfse  5588  elfvmptrab1w  6956  elovmporab  7592  elovmporab1w  7593  ovmpt3rab1  7604  elovmpt3rab1  7606  mpoxopoveq  8149  nfoi  9400  scottex  9778  elmptrab  23742  iundisjf  32569  nnindf  32802  fedgmullem2  33643  bnj1398  35046  bnj1445  35056  bnj1449  35060  nfwlim  35864  finminlem  36362  poimirlem26  37685  poimirlem27  37686  indexa  37772  nfscott  44331  binomcxplemdvbinom  44445  binomcxplemdvsum  44447  binomcxplemnotnn0  44448  infnsuprnmpt  45346  allbutfiinf  45517  supminfrnmpt  45542  supminfxrrnmpt  45568  fnlimfvre  45771  fnlimabslt  45776  dvnprodlem1  46043  stoweidlem16  46113  stoweidlem31  46128  stoweidlem34  46131  stoweidlem35  46132  stoweidlem48  46145  stoweidlem51  46148  stoweidlem53  46150  stoweidlem54  46151  stoweidlem57  46154  stoweidlem59  46156  fourierdlem31  46235  fourierdlem48  46251  fourierdlem51  46254  etransclem32  46363  ovncvrrp  46661  smflim  46874  smflimmpt  46907  smfsupmpt  46912  smfsupxr  46913  smfinfmpt  46916  smflimsuplem7  46923