Theorem nfrabw 3437

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

Syntax hints:   ∧ wa 395  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3400

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3401

This theorem is referenced by:  nfdifOLD  4083  nfinOLD  4178  nfse  5599  elfvmptrab1w  6970  elovmporab  7606  elovmporab1w  7607  ovmpt3rab1  7618  elovmpt3rab1  7620  mpoxopoveq  8163  nfoi  9423  scottex  9801  elmptrab  23775  iundisjf  32646  nnindf  32881  fedgmullem2  33768  bnj1398  35171  bnj1445  35181  bnj1449  35185  nfwlim  35995  finminlem  36493  poimirlem26  37818  poimirlem27  37819  indexa  37905  nfscott  44516  binomcxplemdvbinom  44630  binomcxplemdvsum  44632  binomcxplemnotnn0  44633  infnsuprnmpt  45530  allbutfiinf  45700  supminfrnmpt  45725  supminfxrrnmpt  45751  fnlimfvre  45954  fnlimabslt  45959  dvnprodlem1  46226  stoweidlem16  46296  stoweidlem31  46311  stoweidlem34  46314  stoweidlem35  46315  stoweidlem48  46328  stoweidlem51  46331  stoweidlem53  46333  stoweidlem54  46334  stoweidlem57  46337  stoweidlem59  46339  fourierdlem31  46418  fourierdlem48  46434  fourierdlem51  46437  etransclem32  46546  ovncvrrp  46844  smflim  47057  smflimmpt  47090  smfsupmpt  47095  smfsupxr  47096  smfinfmpt  47099  smflimsuplem7  47106