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

Theorem riotaex 6809
Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
riotaex (𝑥𝐴 𝜓) ∈ V

Proof of Theorem riotaex
StepHypRef Expression
1 df-riota 6805 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
2 iotaex 6050 . 2 (℩𝑥(𝑥𝐴𝜓)) ∈ V
31, 2eqeltri 2840 1 (𝑥𝐴 𝜓) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 2155  Vcvv 3350  cio 6031  crio 6804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-nul 4951
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-sn 4337  df-pr 4339  df-uni 4597  df-iota 6033  df-riota 6805
This theorem is referenced by:  ordtypelem3  8634  dfac8clem  9108  zorn2lem1  9573  subval  10528  1div0  10942  divval  10943  elq  11994  flval  12806  ceilval2  12852  cjval  14130  sqrtval  14265  sqrtf  14391  cidval  16606  cidfn  16608  lubdm  17248  lubval  17253  glbdm  17261  glbval  17266  grpinvval  17731  grpinvfn  17732  pj1val  18375  evlsval  19795  q1pval  24207  ig1pval  24226  coeval  24273  quotval  24341  mirfv  25845  mirf  25849  usgredg2v  26400  frgrncvvdeqlem5  27586  1div0apr  27786  gidval  27826  grpoinvval  27837  grpoinvf  27846  pjhval  28715  pjfni  29019  cnlnadjlem5  29389  nmopadjlei  29406  cdj3lem2  29753  xdivval  30077  cvmlift3lem4  31755  scutval  32358  dmscut  32365  fvtransport  32586  finxpreclem4  33667  poimirlem26  33862  lshpkrlem1  35069  lshpkrlem2  35070  lshpkrlem3  35071  trlval  36121  cdleme31fv  36349  cdleme50f  36501  cdlemksv  36803  cdlemkuu  36854  cdlemk40  36876  cdlemk56  36930  cdlemm10N  37077  cdlemn11a  37166  dihval  37191  dihf11lem  37225  dihatlat  37293  dochfl1  37435  mapdhval  37683  hvmapvalvalN  37720  hdmap1vallem  37756  hdmapval  37787  hdmapfnN  37788  hgmapval  37846  hgmapfnN  37847  mpaaval  38401  wessf1ornlem  40021
  Copyright terms: Public domain W3C validator