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

Theorem nfriota1 6733
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 6726 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 5966 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2864 1 𝑥(𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2103  wnfc 2853  cio 5962  crio 6725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-sn 4286  df-uni 4545  df-iota 5964  df-riota 6726
This theorem is referenced by:  riotaprop  6750  riotass2  6753  riotass  6754  riotaxfrd  6757  lble  11088  riotaneg  11115  zriotaneg  11604  nosupbnd1  32087  nosupbnd2  32089  poimirlem26  33667  riotaocN  34916  ltrniotaval  36288  cdlemksv2  36554  cdlemkuv2  36574  cdlemk36  36620  wessf1ornlem  39787  disjinfi  39796
  Copyright terms: Public domain W3C validator