Theorem nfrabw 3443

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

Syntax hints:   ∧ wa 395  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  {crab 3405

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3406

This theorem is referenced by:  nfdifOLD  4093  nfinOLD  4188  nfse  5612  elfvmptrab1w  6995  elovmporab  7635  elovmporab1w  7636  ovmpt3rab1  7647  elovmpt3rab1  7649  mpoxopoveq  8198  nfoi  9467  scottex  9838  elmptrab  23714  iundisjf  32518  nnindf  32744  fedgmullem2  33626  bnj1398  35024  bnj1445  35034  bnj1449  35038  nfwlim  35810  finminlem  36306  poimirlem26  37640  poimirlem27  37641  indexa  37727  nfscott  44228  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  infnsuprnmpt  45244  allbutfiinf  45416  supminfrnmpt  45441  supminfxrrnmpt  45467  fnlimfvre  45672  fnlimabslt  45677  dvnprodlem1  45944  stoweidlem16  46014  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem48  46046  stoweidlem51  46049  stoweidlem53  46051  stoweidlem54  46052  stoweidlem57  46055  stoweidlem59  46057  fourierdlem31  46136  fourierdlem48  46152  fourierdlem51  46155  etransclem32  46264  ovncvrrp  46562  smflim  46775  smflimmpt  46808  smfsupmpt  46813  smfsupxr  46814  smfinfmpt  46817  smflimsuplem7  46824