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

Theorem nfriota1 7372
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 7365 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 6498 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2902 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  wnfc 2884  cio 6494  crio 7364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-sn 4630  df-uni 4910  df-iota 6496  df-riota 7365
This theorem is referenced by:  riotaprop  7393  riotass2  7396  riotass  7397  riotaxfrd  7400  ttrcltr  9711  lble  12166  riotaneg  12193  zriotaneg  12675  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  poimirlem26  36514  riotaocN  38079  ltrniotaval  39452  cdlemksv2  39718  cdlemkuv2  39738  cdlemk36  39784  disjinfi  43891
  Copyright terms: Public domain W3C validator