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

Theorem nfrab 3325
 Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
nfrab.1 𝑥𝜑
nfrab.2 𝑥𝐴
Assertion
Ref Expression
nfrab 𝑥{𝑦𝐴𝜑}

Proof of Theorem nfrab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-rab 3097 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1767 . . . 4 𝑦
3 nfrab.2 . . . . . . . 8 𝑥𝐴
43nfcri 2926 . . . . . . 7 𝑥 𝑧𝐴
5 eleq1w 2848 . . . . . . 7 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
64, 5dvelimnf 2389 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦𝐴)
7 nfrab.1 . . . . . . 7 𝑥𝜑
87a1i 11 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
96, 8nfand 1860 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦𝐴𝜑))
109adantl 474 . . . 4 ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦𝐴𝜑))
112, 10nfabd2 2953 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
1211mptru 1514 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
131, 12nfcxfr 2930 1 𝑥{𝑦𝐴𝜑}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 387  ∀wal 1505  ⊤wtru 1508  Ⅎwnf 1746   ∈ wcel 2050  {cab 2758  Ⅎwnfc 2916  {crab 3092 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097 This theorem is referenced by:  nfdif  3992  nfin  4080  nfse  5382  elfvmptrab1  6620  elovmporab  7210  elovmporab1  7211  ovmpt3rab1  7221  elovmpt3rab1  7223  mpoxopoveq  7688  nfoi  8773  scottex  9108  elmptrab  22139  iundisjf  30105  nnindf  30288  fedgmullem2  30661  bnj1398  31957  bnj1445  31967  bnj1449  31971  nfwlim  32636  finminlem  33193  poimirlem26  34365  poimirlem27  34366  indexa  34456  nfscott  39956  binomcxplemdvbinom  40107  binomcxplemdvsum  40109  binomcxplemnotnn0  40110  infnsuprnmpt  40956  allbutfiinf  41131  supminfrnmpt  41156  supminfxrrnmpt  41184  fnlimfvre  41392  fnlimabslt  41397  dvnprodlem1  41667  stoweidlem16  41738  stoweidlem31  41753  stoweidlem34  41756  stoweidlem35  41757  stoweidlem48  41770  stoweidlem51  41773  stoweidlem53  41775  stoweidlem54  41776  stoweidlem57  41779  stoweidlem59  41781  fourierdlem31  41860  fourierdlem48  41876  fourierdlem51  41879  etransclem32  41988  ovncvrrp  42283  smflim  42490  smflimmpt  42521  smfsupmpt  42526  smfsupxr  42527  smfinfmpt  42530  smflimsuplem7  42537
 Copyright terms: Public domain W3C validator