Theorem riotaex 7319

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3439  ℩cio 6445  ℩crio 7314

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 2707  ax-nul 5250

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 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-sn 4580  df-pr 4582  df-uni 4863  df-iota 6447  df-riota 7315

This theorem is referenced by:  ordtypelem3  9427  dfac8clem  9944  zorn2lem1  10408  subval  11373  1div0  11798  1div0OLD  11799  divval  11800  elq  12865  flval  13716  ceilval2  13762  cjval  15027  sqrtval  15162  sqrtf  15289  cidval  17602  cidfn  17604  lubdm  18274  lubval  18279  glbdm  18287  glbval  18292  grpinvfval  18910  grpinvval  18912  grpinvfn  18913  pj1val  19626  evlsval  22043  q1pval  26118  ig1pval  26139  coeval  26186  quotval  26258  scutval  27776  dmscut  27787  divsval  28169  mirfv  28709  mirf  28713  usgredg2v  29281  frgrncvvdeqlem5  30359  1div0apr  30524  gidval  30568  grpoinvval  30579  grpoinvf  30588  pjhval  31453  pjfni  31757  cnlnadjlem5  32127  nmopadjlei  32144  cdj3lem2  32491  xdivval  32979  cvmlift3lem4  35495  fvtransport  36205  weiunlem2  36636  finxpreclem4  37568  poimirlem26  37816  lshpkrlem1  39405  lshpkrlem2  39406  lshpkrlem3  39407  trlval  40457  cdleme31fv  40685  cdleme50f  40837  cdlemksv  41139  cdlemkuu  41190  cdlemk40  41212  cdlemk56  41266  cdlemm10N  41413  cdlemn11a  41502  dihval  41527  dihf11lem  41561  dihatlat  41629  dochfl1  41771  mapdhval  42019  hvmapvalvalN  42056  hdmap1vallem  42092  hdmapval  42123  hdmapfnN  42124  hgmapval  42182  hgmapfnN  42183  resubval  42659  redivvald  42734  mpaaval  43430  wessf1ornlem  45466