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

Theorem nfrab 3272
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 3070 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1878 . . . 4 𝑦
3 nfrab.2 . . . . . . . 8 𝑥𝐴
43nfcri 2907 . . . . . . 7 𝑥 𝑧𝐴
5 eleq1w 2833 . . . . . . 7 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
64, 5dvelimnf 2489 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦𝐴)
7 nfrab.1 . . . . . . 7 𝑥𝜑
87a1i 11 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
96, 8nfand 1978 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦𝐴𝜑))
109adantl 467 . . . 4 ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦𝐴𝜑))
112, 10nfabd2 2933 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
1211trud 1641 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
131, 12nfcxfr 2911 1 𝑥{𝑦𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382  wal 1629  wtru 1632  wnf 1856  wcel 2145  {cab 2757  wnfc 2900  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070
This theorem is referenced by:  nfdif  3882  nfin  3969  nfse  5224  elfvmptrab1  6447  elovmpt2rab  7027  elovmpt2rab1  7028  ovmpt3rab1  7038  elovmpt3rab1  7040  mpt2xopoveq  7497  nfoi  8575  scottex  8912  elmptrab  21851  iundisjf  29740  nnindf  29905  bnj1398  31440  bnj1445  31450  bnj1449  31454  nfwlim  32104  finminlem  32649  poimirlem26  33768  poimirlem27  33769  indexa  33860  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  infnsuprnmpt  39983  allbutfiinf  40163  supminfrnmpt  40188  supminfxrrnmpt  40217  fnlimfvre  40424  fnlimabslt  40429  dvnprodlem1  40679  stoweidlem16  40750  stoweidlem31  40765  stoweidlem34  40768  stoweidlem35  40769  stoweidlem48  40782  stoweidlem51  40785  stoweidlem53  40787  stoweidlem54  40788  stoweidlem57  40791  stoweidlem59  40793  fourierdlem31  40872  fourierdlem48  40888  fourierdlem51  40891  etransclem32  41000  ovncvrrp  41298  smflim  41505  smflimmpt  41536  smfsupmpt  41541  smfsupxr  41542  smfinfmpt  41545  smflimsuplem7  41552
  Copyright terms: Public domain W3C validator