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

Theorem nfriota1 6583
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 6576 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 5822 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2759 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 1987  wnfc 2748  cio 5818  crio 6575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-sn 4156  df-uni 4410  df-iota 5820  df-riota 6576
This theorem is referenced by:  riotaprop  6600  riotass2  6603  riotass  6604  riotaxfrd  6607  lble  10935  riotaneg  10962  zriotaneg  11451  poimirlem26  33106  riotaocN  34015  ltrniotaval  35388  cdlemksv2  35654  cdlemkuv2  35674  cdlemk36  35720  wessf1ornlem  38880  disjinfi  38889
  Copyright terms: Public domain W3C validator