Theorem riotaex 7331

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3442  ℩cio 6456  ℩crio 7326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5255

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458  df-riota 7327

This theorem is referenced by:  ordtypelem3  9439  dfac8clem  9956  zorn2lem1  10420  subval  11385  1div0  11810  1div0OLD  11811  divval  11812  elq  12877  flval  13728  ceilval2  13774  cjval  15039  sqrtval  15174  sqrtf  15301  cidval  17614  cidfn  17616  lubdm  18286  lubval  18291  glbdm  18299  glbval  18304  grpinvfval  18925  grpinvval  18927  grpinvfn  18928  pj1val  19641  evlsval  22058  q1pval  26133  ig1pval  26154  coeval  26201  quotval  26273  cutsval  27793  dmcuts  27804  divsval  28202  mirfv  28746  mirf  28750  usgredg2v  29318  frgrncvvdeqlem5  30396  1div0apr  30561  gidval  30606  grpoinvval  30617  grpoinvf  30626  pjhval  31491  pjfni  31795  cnlnadjlem5  32165  nmopadjlei  32182  cdj3lem2  32529  xdivval  33017  cvmlift3lem4  35544  fvtransport  36254  weiunlem  36685  finxpreclem4  37676  poimirlem26  37926  lshpkrlem1  39515  lshpkrlem2  39516  lshpkrlem3  39517  trlval  40567  cdleme31fv  40795  cdleme50f  40947  cdlemksv  41249  cdlemkuu  41300  cdlemk40  41322  cdlemk56  41376  cdlemm10N  41523  cdlemn11a  41612  dihval  41637  dihf11lem  41671  dihatlat  41739  dochfl1  41881  mapdhval  42129  hvmapvalvalN  42166  hdmap1vallem  42202  hdmapval  42233  hdmapfnN  42234  hgmapval  42292  hgmapfnN  42293  resubval  42766  redivvald  42841  mpaaval  43537  wessf1ornlem  45573