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

Theorem nfrab 3319
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 3112 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1886 . . . 4 𝑦
3 nfrab.2 . . . . . . . 8 𝑥𝐴
43nfcri 2949 . . . . . . 7 𝑥 𝑧𝐴
5 eleq1w 2875 . . . . . . 7 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
64, 5dvelimnf 2503 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦𝐴)
7 nfrab.1 . . . . . . 7 𝑥𝜑
87a1i 11 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
96, 8nfand 1988 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦𝐴𝜑))
109adantl 469 . . . 4 ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦𝐴𝜑))
112, 10nfabd2 2975 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
1211mptru 1645 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
131, 12nfcxfr 2953 1 𝑥{𝑦𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 384  wal 1635  wtru 1638  wnf 1863  wcel 2157  {cab 2799  wnfc 2942  {crab 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112
This theorem is referenced by:  nfdif  3937  nfin  4024  nfse  5293  elfvmptrab1  6529  elovmpt2rab  7113  elovmpt2rab1  7114  ovmpt3rab1  7124  elovmpt3rab1  7126  mpt2xopoveq  7583  nfoi  8661  scottex  8998  elmptrab  21848  iundisjf  29733  nnindf  29898  bnj1398  31430  bnj1445  31440  bnj1449  31444  nfwlim  32093  finminlem  32638  poimirlem26  33750  poimirlem27  33751  indexa  33842  binomcxplemdvbinom  39053  binomcxplemdvsum  39055  binomcxplemnotnn0  39056  infnsuprnmpt  39949  allbutfiinf  40127  supminfrnmpt  40152  supminfxrrnmpt  40181  fnlimfvre  40387  fnlimabslt  40392  dvnprodlem1  40642  stoweidlem16  40713  stoweidlem31  40728  stoweidlem34  40731  stoweidlem35  40732  stoweidlem48  40745  stoweidlem51  40748  stoweidlem53  40750  stoweidlem54  40751  stoweidlem57  40754  stoweidlem59  40756  fourierdlem31  40835  fourierdlem48  40851  fourierdlem51  40854  etransclem32  40963  ovncvrrp  41261  smflim  41468  smflimmpt  41499  smfsupmpt  41504  smfsupxr  41505  smfinfmpt  41508  smflimsuplem7  41515
  Copyright terms: Public domain W3C validator