Theorem riotaex 7360

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

Syntax hints:   ∧ wa 395   ∈ wcel 2107  Vcvv 3457  ℩cio 6478  ℩crio 7355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5273

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-sn 4600  df-pr 4602  df-uni 4881  df-iota 6480  df-riota 7356

This theorem is referenced by:  ordtypelem3  9526  dfac8clem  10038  zorn2lem1  10502  subval  11465  1div0  11888  1div0OLD  11889  divval  11890  elq  12958  flval  13800  ceilval2  13846  cjval  15108  sqrtval  15243  sqrtf  15369  cidval  17674  cidfn  17676  lubdm  18346  lubval  18351  glbdm  18359  glbval  18364  grpinvfval  18946  grpinvval  18948  grpinvfn  18949  pj1val  19661  evlsval  22029  q1pval  26097  ig1pval  26118  coeval  26165  quotval  26237  scutval  27748  dmscut  27759  divsval  28118  mirfv  28567  mirf  28571  usgredg2v  29138  frgrncvvdeqlem5  30216  1div0apr  30381  gidval  30425  grpoinvval  30436  grpoinvf  30445  pjhval  31310  pjfni  31614  cnlnadjlem5  31984  nmopadjlei  32001  cdj3lem2  32348  xdivval  32811  cvmlift3lem4  35265  fvtransport  35971  weiunlem2  36402  finxpreclem4  37333  poimirlem26  37591  lshpkrlem1  39049  lshpkrlem2  39050  lshpkrlem3  39051  trlval  40102  cdleme31fv  40330  cdleme50f  40482  cdlemksv  40784  cdlemkuu  40835  cdlemk40  40857  cdlemk56  40911  cdlemm10N  41058  cdlemn11a  41147  dihval  41172  dihf11lem  41206  dihatlat  41274  dochfl1  41416  mapdhval  41664  hvmapvalvalN  41701  hdmap1vallem  41737  hdmapval  41768  hdmapfnN  41769  hgmapval  41827  hgmapfnN  41828  resubval  42335  mpaaval  43100  wessf1ornlem  45136