MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrabw Structured version   Visualization version   GIF version

Theorem nfrabw 3443
Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3446 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2371. (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
StepHypRef Expression
1 df-rab 3411 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1807 . . . 4 𝑦
3 nfrabw.2 . . . . . . 7 𝑥𝐴
43nfcri 2895 . . . . . 6 𝑥 𝑦𝐴
5 nfrabw.1 . . . . . 6 𝑥𝜑
64, 5nfan 1903 . . . . 5 𝑥(𝑦𝐴𝜑)
76a1i 11 . . . 4 (⊤ → Ⅎ𝑥(𝑦𝐴𝜑))
82, 7nfabdw 2931 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
98mptru 1549 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
101, 9nfcxfr 2906 1 𝑥{𝑦𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 397  wtru 1543  wnf 1786  wcel 2107  {cab 2714  wnfc 2888  {crab 3410
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-rab 3411
This theorem is referenced by:  nfdif  4090  nfin  4181  nfse  5613  elfvmptrab1w  6979  elovmporab  7604  elovmporab1w  7605  ovmpt3rab1  7616  elovmpt3rab1  7618  mpoxopoveq  8155  nfoi  9457  scottex  9828  elmptrab  23194  iundisjf  31549  nnindf  31757  fedgmullem2  32365  bnj1398  33686  bnj1445  33696  bnj1449  33700  nfwlim  34436  finminlem  34819  poimirlem26  36133  poimirlem27  36134  indexa  36221  nfscott  42593  binomcxplemdvbinom  42707  binomcxplemdvsum  42709  binomcxplemnotnn0  42710  infnsuprnmpt  43552  allbutfiinf  43729  supminfrnmpt  43754  supminfxrrnmpt  43780  fnlimfvre  43989  fnlimabslt  43994  dvnprodlem1  44261  stoweidlem16  44331  stoweidlem31  44346  stoweidlem34  44349  stoweidlem35  44350  stoweidlem48  44363  stoweidlem51  44366  stoweidlem53  44368  stoweidlem54  44369  stoweidlem57  44372  stoweidlem59  44374  fourierdlem31  44453  fourierdlem48  44469  fourierdlem51  44472  etransclem32  44581  ovncvrrp  44879  smflim  45092  smflimmpt  45125  smfsupmpt  45130  smfsupxr  45131  smfinfmpt  45134  smflimsuplem7  45141
  Copyright terms: Public domain W3C validator