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

Theorem nfriota1 6518
 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 6511 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 5770 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2749 1 𝑥(𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   ∈ wcel 1977  Ⅎwnfc 2738  ℩cio 5766  ℩crio 6510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-sn 4126  df-uni 4373  df-iota 5768  df-riota 6511 This theorem is referenced by:  riotaprop  6534  riotass2  6537  riotass  6538  riotaxfrd  6541  lble  10854  riotaneg  10879  zriotaneg  11367  poimirlem26  32605  riotaocN  33514  ltrniotaval  34887  cdlemksv2  35153  cdlemkuv2  35173  cdlemk36  35219  wessf1ornlem  38366  disjinfi  38375
 Copyright terms: Public domain W3C validator