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

Theorem riotaex 6575
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 6571 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
2 iotaex 5832 . 2 (℩𝑥(𝑥𝐴𝜓)) ∈ V
31, 2eqeltri 2694 1 (𝑥𝐴 𝜓) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 1987  Vcvv 3189  cio 5813  crio 6570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-sn 4154  df-pr 4156  df-uni 4408  df-iota 5815  df-riota 6571
This theorem is referenced by:  ordtypelem3  8377  dfac8clem  8807  zorn2lem1  9270  subval  10224  1div0  10638  divval  10639  elq  11742  flval  12543  ceilval2  12589  cjval  13784  sqrtval  13919  sqrtf  14045  cidval  16270  cidfn  16272  lubdm  16911  lubval  16916  glbdm  16924  glbval  16929  grpinvval  17393  grpinvfn  17394  pj1val  18040  evlsval  19451  q1pval  23834  ig1pval  23853  coeval  23900  quotval  23968  mirfv  25468  mirf  25472  usgredg2v  26029  frgrncvvdeqlem6  27049  1div0apr  27195  gidval  27236  grpoinvval  27247  grpoinvf  27256  pjhval  28126  pjfni  28430  cnlnadjlem5  28800  nmopadjlei  28817  cdj3lem2  29164  xdivval  29436  cvmlift3lem4  31047  fvtransport  31816  finxpreclem4  32898  poimirlem26  33102  lshpkrlem1  33912  lshpkrlem2  33913  lshpkrlem3  33914  trlval  34964  cdleme31fv  35193  cdleme50f  35345  cdlemksv  35647  cdlemkuu  35698  cdlemk40  35720  cdlemk56  35774  cdlemm10N  35922  cdlemn11a  36011  dihval  36036  dihf11lem  36070  dihatlat  36138  dochfl1  36280  mapdhval  36528  hvmapvalvalN  36565  hdmap1vallem  36602  hdmapval  36635  hdmapfnN  36636  hgmapval  36694  hgmapfnN  36695  mpaaval  37237  wessf1ornlem  38876
  Copyright terms: Public domain W3C validator