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

Theorem nfriota1 7395
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 7388 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 6518 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2901 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2106  wnfc 2888  cio 6514  crio 7387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-sn 4632  df-uni 4913  df-iota 6516  df-riota 7388
This theorem is referenced by:  riotaprop  7415  riotass2  7418  riotass  7419  riotaxfrd  7422  ttrcltr  9754  lble  12218  riotaneg  12245  zriotaneg  12729  nosupbnd1  27774  nosupbnd2  27776  noinfbnd1  27789  noinfbnd2  27791  poimirlem26  37633  riotaocN  39191  ltrniotaval  40564  cdlemksv2  40830  cdlemkuv2  40850  cdlemk36  40896  disjinfi  45135
  Copyright terms: Public domain W3C validator