Theorem riotaex 7307

Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)

Assertion

Ref	Expression
riotaex	⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V

Proof of Theorem riotaex

Step	Hyp	Ref	Expression
1		df-riota 7303	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
2		iotaex 6457	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V
3	1, 2	eqeltri 2827	1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2111  Vcvv 3436  ℩cio 6435  ℩crio 7302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-riota 7303

This theorem is referenced by:  ordtypelem3  9406  dfac8clem  9923  zorn2lem1  10387  subval  11351  1div0  11776  1div0OLD  11777  divval  11778  elq  12848  flval  13698  ceilval2  13744  cjval  15009  sqrtval  15144  sqrtf  15271  cidval  17583  cidfn  17585  lubdm  18255  lubval  18260  glbdm  18268  glbval  18273  grpinvfval  18891  grpinvval  18893  grpinvfn  18894  pj1val  19607  evlsval  22021  q1pval  26087  ig1pval  26108  coeval  26155  quotval  26227  scutval  27741  dmscut  27752  divsval  28128  mirfv  28634  mirf  28638  usgredg2v  29205  frgrncvvdeqlem5  30283  1div0apr  30448  gidval  30492  grpoinvval  30503  grpoinvf  30512  pjhval  31377  pjfni  31681  cnlnadjlem5  32051  nmopadjlei  32068  cdj3lem2  32415  xdivval  32899  cvmlift3lem4  35366  fvtransport  36076  weiunlem2  36507  finxpreclem4  37438  poimirlem26  37685  lshpkrlem1  39208  lshpkrlem2  39209  lshpkrlem3  39210  trlval  40260  cdleme31fv  40488  cdleme50f  40640  cdlemksv  40942  cdlemkuu  40993  cdlemk40  41015  cdlemk56  41069  cdlemm10N  41216  cdlemn11a  41305  dihval  41330  dihf11lem  41364  dihatlat  41432  dochfl1  41574  mapdhval  41822  hvmapvalvalN  41859  hdmap1vallem  41895  hdmapval  41926  hdmapfnN  41927  hgmapval  41985  hgmapfnN  41986  resubval  42459  redivvald  42534  mpaaval  43243  wessf1ornlem  45281