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  32667  nnindf  32902  fedgmullem2  33789  bnj1398  35192  bnj1445  35202  bnj1449  35206  nfwlim  36016  finminlem  36514  poimirlem26  37849  poimirlem27  37850  indexa  37936  nfscott  44547  binomcxplemdvbinom  44661  binomcxplemdvsum  44663  binomcxplemnotnn0  44664  infnsuprnmpt  45561  allbutfiinf  45731  supminfrnmpt  45756  supminfxrrnmpt  45782  fnlimfvre  45985  fnlimabslt  45990  dvnprodlem1  46257  stoweidlem16  46327  stoweidlem31  46342  stoweidlem34  46345  stoweidlem35  46346  stoweidlem48  46359  stoweidlem51  46362  stoweidlem53  46364  stoweidlem54  46365  stoweidlem57  46368  stoweidlem59  46370  fourierdlem31  46449  fourierdlem48  46465  fourierdlem51  46468  etransclem32  46577  ovncvrrp  46875  smflim  47088  smflimmpt  47121  smfsupmpt  47126  smfsupxr  47127  smfinfmpt  47130  smflimsuplem7  47137