Theorem riotaex 7317

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3427  ℩cio 6441  ℩crio 7312

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 5230

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 2931  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-sn 4558  df-pr 4560  df-uni 4841  df-iota 6443  df-riota 7313

This theorem is referenced by:  ordtypelem3  9424  dfac8clem  9943  zorn2lem1  10407  subval  11373  1div0  11798  1div0OLD  11799  divval  11800  elq  12889  flval  13742  ceilval2  13788  cjval  15053  sqrtval  15188  sqrtf  15315  cidval  17632  cidfn  17634  lubdm  18304  lubval  18309  glbdm  18317  glbval  18322  grpinvfval  18943  grpinvval  18945  grpinvfn  18946  pj1val  19659  evlsval  22053  q1pval  26108  ig1pval  26129  coeval  26176  quotval  26246  cutsval  27760  dmcuts  27771  divsval  28169  mirfv  28712  mirf  28716  usgredg2v  29284  frgrncvvdeqlem5  30361  1div0apr  30526  gidval  30571  grpoinvval  30582  grpoinvf  30591  pjhval  31456  pjfni  31760  cnlnadjlem5  32130  nmopadjlei  32147  cdj3lem2  32494  xdivval  32966  cvmlift3lem4  35492  fvtransport  36202  weiunlem  36633  finxpreclem4  37698  poimirlem26  37955  lshpkrlem1  39544  lshpkrlem2  39545  lshpkrlem3  39546  trlval  40596  cdleme31fv  40824  cdleme50f  40976  cdlemksv  41278  cdlemkuu  41329  cdlemk40  41351  cdlemk56  41405  cdlemm10N  41552  cdlemn11a  41641  dihval  41666  dihf11lem  41700  dihatlat  41768  dochfl1  41910  mapdhval  42158  hvmapvalvalN  42195  hdmap1vallem  42231  hdmapval  42262  hdmapfnN  42263  hgmapval  42321  hgmapfnN  42322  resubval  42787  redivvald  42862  mpaaval  43567  wessf1ornlem  45603