Theorem riotaex 7369

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

Syntax hints:   ∧ wa 397   ∈ wcel 2107  Vcvv 3475  ℩cio 6494  ℩crio 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-riota 7365

This theorem is referenced by:  ordtypelem3  9515  dfac8clem  10027  zorn2lem1  10491  subval  11451  1div0  11873  divval  11874  elq  12934  flval  13759  ceilval2  13805  cjval  15049  sqrtval  15184  sqrtf  15310  cidval  17621  cidfn  17623  lubdm  18304  lubval  18309  glbdm  18317  glbval  18322  grpinvfval  18863  grpinvval  18865  grpinvfn  18866  pj1val  19563  evlsval  21649  q1pval  25671  ig1pval  25690  coeval  25737  quotval  25805  scutval  27301  dmscut  27312  divsval  27637  mirfv  27907  mirf  27911  usgredg2v  28484  frgrncvvdeqlem5  29556  1div0apr  29721  gidval  29765  grpoinvval  29776  grpoinvf  29785  pjhval  30650  pjfni  30954  cnlnadjlem5  31324  nmopadjlei  31341  cdj3lem2  31688  xdivval  32085  cvmlift3lem4  34313  fvtransport  35004  finxpreclem4  36275  poimirlem26  36514  lshpkrlem1  37980  lshpkrlem2  37981  lshpkrlem3  37982  trlval  39033  cdleme31fv  39261  cdleme50f  39413  cdlemksv  39715  cdlemkuu  39766  cdlemk40  39788  cdlemk56  39842  cdlemm10N  39989  cdlemn11a  40078  dihval  40103  dihf11lem  40137  dihatlat  40205  dochfl1  40347  mapdhval  40595  hvmapvalvalN  40632  hdmap1vallem  40668  hdmapval  40699  hdmapfnN  40700  hgmapval  40758  hgmapfnN  40759  resubval  41240  mpaaval  41893  wessf1ornlem  43882