Theorem nfrabw 3446

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2109  {cab 2708  Ⅎwnfc 2877  {crab 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409

This theorem is referenced by:  nfdifOLD  4096  nfinOLD  4191  nfse  5615  elfvmptrab1w  6998  elovmporab  7638  elovmporab1w  7639  ovmpt3rab1  7650  elovmpt3rab1  7652  mpoxopoveq  8201  nfoi  9474  scottex  9845  elmptrab  23721  iundisjf  32525  nnindf  32751  fedgmullem2  33633  bnj1398  35031  bnj1445  35041  bnj1449  35045  nfwlim  35817  finminlem  36313  poimirlem26  37647  poimirlem27  37648  indexa  37734  nfscott  44235  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  infnsuprnmpt  45251  allbutfiinf  45423  supminfrnmpt  45448  supminfxrrnmpt  45474  fnlimfvre  45679  fnlimabslt  45684  dvnprodlem1  45951  stoweidlem16  46021  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem48  46053  stoweidlem51  46056  stoweidlem53  46058  stoweidlem54  46059  stoweidlem57  46062  stoweidlem59  46064  fourierdlem31  46143  fourierdlem48  46159  fourierdlem51  46162  etransclem32  46271  ovncvrrp  46569  smflim  46782  smflimmpt  46815  smfsupmpt  46820  smfsupxr  46821  smfinfmpt  46824  smflimsuplem7  46831