Theorem riotaex 7310

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 7306	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
2		iotaex 6458	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V
3	1, 2	eqeltri 2824	1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3436  ℩cio 6436  ℩crio 7305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-riota 7306

This theorem is referenced by:  ordtypelem3  9412  dfac8clem  9926  zorn2lem1  10390  subval  11354  1div0  11779  1div0OLD  11780  divval  11781  elq  12851  flval  13698  ceilval2  13744  cjval  15009  sqrtval  15144  sqrtf  15271  cidval  17583  cidfn  17585  lubdm  18255  lubval  18260  glbdm  18268  glbval  18273  grpinvfval  18857  grpinvval  18859  grpinvfn  18860  pj1val  19574  evlsval  21991  q1pval  26058  ig1pval  26079  coeval  26126  quotval  26198  scutval  27712  dmscut  27723  divsval  28099  mirfv  28605  mirf  28609  usgredg2v  29176  frgrncvvdeqlem5  30251  1div0apr  30416  gidval  30460  grpoinvval  30471  grpoinvf  30480  pjhval  31345  pjfni  31649  cnlnadjlem5  32019  nmopadjlei  32036  cdj3lem2  32383  xdivval  32868  cvmlift3lem4  35315  fvtransport  36026  weiunlem2  36457  finxpreclem4  37388  poimirlem26  37646  lshpkrlem1  39109  lshpkrlem2  39110  lshpkrlem3  39111  trlval  40161  cdleme31fv  40389  cdleme50f  40541  cdlemksv  40843  cdlemkuu  40894  cdlemk40  40916  cdlemk56  40970  cdlemm10N  41117  cdlemn11a  41206  dihval  41231  dihf11lem  41265  dihatlat  41333  dochfl1  41475  mapdhval  41723  hvmapvalvalN  41760  hdmap1vallem  41796  hdmapval  41827  hdmapfnN  41828  hgmapval  41886  hgmapfnN  41887  resubval  42360  redivvald  42435  mpaaval  43144  wessf1ornlem  45183