Theorem nfrabw 3450

Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3451 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2403. (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 3415	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nfrabw.2	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfrabw.1	. . . 4 ⊢ Ⅎ𝑥𝜑
5	3, 4	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)
6	5	nfab 2930	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
7	1, 6	nfcxfr 2922	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2145  {cab 2740  Ⅎwnfc 2909  {crab 3414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415

This theorem is used by:  nfse  5633  elfvmptrab1w  7018  elfvmptrab1  7019  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  ovmpt3rab1  7675  elovmpt3rab1  7677  mpoxopoveq  8220  nfoi  9489  nfscott  9874  scottexOLD  9876  elmptrab  24052  iundisjf  33047  nnindf  33275  fedgmullem2  34125  bnj1398  35528  bnj1445  35538  bnj1449  35542  nfwlim  36384  finminlem  36922  poimirlem26  38380  poimirlem27  38381  indexa  38468  binomcxplemdvbinom  45162  binomcxplemdvsum  45164  binomcxplemnotnn0  45165  infnsuprnmpt  46064  allbutfiinf  46233  supminfrnmpt  46258  supminfxrrnmpt  46284  fnlimfvre  46487  fnlimabslt  46492  dvnprodlem1  46759  stoweidlem16  46829  stoweidlem31  46844  stoweidlem34  46847  stoweidlem35  46848  stoweidlem48  46861  stoweidlem51  46864  stoweidlem53  46866  stoweidlem54  46867  stoweidlem57  46870  stoweidlem59  46872  fourierdlem31  46951  fourierdlem48  46967  fourierdlem51  46970  etransclem32  47079  ovncvrrp  47377  smflim  47590  smflimmpt  47623  smfsupmpt  47628  smfsupxr  47629  smfinfmpt  47632  smflimsuplem7  47639