Theorem nfrabw 3469

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

Syntax hints:   ∧ wa 397  ⊤wtru 1543  Ⅎwnf 1786   ∈ wcel 2107  {cab 2710  Ⅎwnfc 2884  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434

This theorem is referenced by:  nfdif  4126  nfin  4217  nfse  5652  elfvmptrab1w  7025  elovmporab  7652  elovmporab1w  7653  ovmpt3rab1  7664  elovmpt3rab1  7666  mpoxopoveq  8204  nfoi  9509  scottex  9880  elmptrab  23331  iundisjf  31820  nnindf  32025  fedgmullem2  32715  bnj1398  34045  bnj1445  34055  bnj1449  34059  nfwlim  34794  finminlem  35203  poimirlem26  36514  poimirlem27  36515  indexa  36601  nfscott  42998  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  infnsuprnmpt  43954  allbutfiinf  44130  supminfrnmpt  44155  supminfxrrnmpt  44181  fnlimfvre  44390  fnlimabslt  44395  dvnprodlem1  44662  stoweidlem16  44732  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem48  44764  stoweidlem51  44767  stoweidlem53  44769  stoweidlem54  44770  stoweidlem57  44773  stoweidlem59  44775  fourierdlem31  44854  fourierdlem48  44870  fourierdlem51  44873  etransclem32  44982  ovncvrrp  45280  smflim  45493  smflimmpt  45526  smfsupmpt  45531  smfsupxr  45532  smfinfmpt  45535  smflimsuplem7  45542