Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfriota1 Structured version   Unicode version

Theorem nfriota1 6270
 Description: The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
Assertion
Ref Expression
nfriota1
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem nfriota1
StepHypRef Expression
1 df-riota 6263 . 2
2 nfiota1 5563 . 2
31, 2nfcxfr 2582 1
 Colors of variables: wff setvar class Syntax hints:   wa 370   wcel 1868  wnfc 2570  cio 5559  crio 6262 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-sn 3997  df-uni 4217  df-iota 5561  df-riota 6263 This theorem is referenced by:  riotaprop  6286  riotass2  6289  riotass  6290  riotaxfrd  6293  lble  10558  riotaneg  10586  zriotaneg  11049  poimirlem26  31877  riotaocN  32691  ltrniotaval  34064  cdlemksv2  34330  cdlemkuv2  34350  cdlemk36  34396  wessf1ornlem  37306  disjinfi  37315
 Copyright terms: Public domain W3C validator