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

Theorem nfriota1 7374
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 7367 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 6496 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2899 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 394  wcel 2104  wnfc 2881  cio 6492  crio 7366
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-v 3474  df-in 3954  df-ss 3964  df-sn 4628  df-uni 4908  df-iota 6494  df-riota 7367
This theorem is referenced by:  riotaprop  7395  riotass2  7398  riotass  7399  riotaxfrd  7402  ttrcltr  9713  lble  12170  riotaneg  12197  zriotaneg  12679  nosupbnd1  27453  nosupbnd2  27455  noinfbnd1  27468  noinfbnd2  27470  poimirlem26  36817  riotaocN  38382  ltrniotaval  39755  cdlemksv2  40021  cdlemkuv2  40041  cdlemk36  40087  disjinfi  44189
  Copyright terms: Public domain W3C validator