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

Theorem nfrabw 3475
Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3478 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2377. (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
StepHypRef Expression
1 df-rab 3437 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1804 . . . 4 𝑦
3 nfrabw.2 . . . . . . 7 𝑥𝐴
43nfcri 2897 . . . . . 6 𝑥 𝑦𝐴
5 nfrabw.1 . . . . . 6 𝑥𝜑
64, 5nfan 1899 . . . . 5 𝑥(𝑦𝐴𝜑)
76a1i 11 . . . 4 (⊤ → Ⅎ𝑥(𝑦𝐴𝜑))
82, 7nfabdw 2927 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
98mptru 1547 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
101, 9nfcxfr 2903 1 𝑥{𝑦𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 395  wtru 1541  wnf 1783  wcel 2108  {cab 2714  wnfc 2890  {crab 3436
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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437
This theorem is referenced by:  nfdifOLD  4130  nfinOLD  4225  nfse  5659  elfvmptrab1w  7043  elovmporab  7679  elovmporab1w  7680  ovmpt3rab1  7691  elovmpt3rab1  7693  mpoxopoveq  8244  nfoi  9554  scottex  9925  elmptrab  23835  iundisjf  32602  nnindf  32821  fedgmullem2  33681  bnj1398  35048  bnj1445  35058  bnj1449  35062  nfwlim  35823  finminlem  36319  poimirlem26  37653  poimirlem27  37654  indexa  37740  nfscott  44258  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  infnsuprnmpt  45257  allbutfiinf  45431  supminfrnmpt  45456  supminfxrrnmpt  45482  fnlimfvre  45689  fnlimabslt  45694  dvnprodlem1  45961  stoweidlem16  46031  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem48  46063  stoweidlem51  46066  stoweidlem53  46068  stoweidlem54  46069  stoweidlem57  46072  stoweidlem59  46074  fourierdlem31  46153  fourierdlem48  46169  fourierdlem51  46172  etransclem32  46281  ovncvrrp  46579  smflim  46792  smflimmpt  46825  smfsupmpt  46830  smfsupxr  46831  smfinfmpt  46834  smflimsuplem7  46841
  Copyright terms: Public domain W3C validator