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 6516 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2903 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2108  wnfc 2890  cio 6512  crio 7387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-sn 4627  df-uni 4908  df-iota 6514  df-riota 7388
This theorem is referenced by:  riotaprop  7415  riotass2  7418  riotass  7419  riotaxfrd  7422  ttrcltr  9756  lble  12220  riotaneg  12247  zriotaneg  12731  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  poimirlem26  37653  riotaocN  39210  ltrniotaval  40583  cdlemksv2  40849  cdlemkuv2  40869  cdlemk36  40915  disjinfi  45197
  Copyright terms: Public domain W3C validator