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  31851  nnindf  32056  fedgmullem2  32746  bnj1398  34076  bnj1445  34086  bnj1449  34090  nfwlim  34825  finminlem  35251  poimirlem26  36562  poimirlem27  36563  indexa  36649  nfscott  43046  binomcxplemdvbinom  43160  binomcxplemdvsum  43162  binomcxplemnotnn0  43163  infnsuprnmpt  44002  allbutfiinf  44178  supminfrnmpt  44203  supminfxrrnmpt  44229  fnlimfvre  44438  fnlimabslt  44443  dvnprodlem1  44710  stoweidlem16  44780  stoweidlem31  44795  stoweidlem34  44798  stoweidlem35  44799  stoweidlem48  44812  stoweidlem51  44815  stoweidlem53  44817  stoweidlem54  44818  stoweidlem57  44821  stoweidlem59  44823  fourierdlem31  44902  fourierdlem48  44918  fourierdlem51  44921  etransclem32  45030  ovncvrrp  45328  smflim  45541  smflimmpt  45574  smfsupmpt  45579  smfsupxr  45580  smfinfmpt  45583  smflimsuplem7  45590