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

Theorem nfriota1 7116
 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 7109 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
2 nfiota1 6297 . 2 𝑥(℩𝑥(𝑥𝐴𝜑))
31, 2nfcxfr 2918 1 𝑥(𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 400   ∈ wcel 2112  Ⅎwnfc 2900  ℩cio 6293  ℩crio 7108 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-v 3412  df-in 3866  df-ss 3876  df-sn 4524  df-uni 4800  df-iota 6295  df-riota 7109 This theorem is referenced by:  riotaprop  7136  riotass2  7139  riotass  7140  riotaxfrd  7143  lble  11630  riotaneg  11657  zriotaneg  12136  nosupbnd1  33483  nosupbnd2  33485  noinfbnd1  33498  noinfbnd2  33500  poimirlem26  35364  riotaocN  36786  ltrniotaval  38158  cdlemksv2  38424  cdlemkuv2  38444  cdlemk36  38490  disjinfi  42191
 Copyright terms: Public domain W3C validator