Theorem riotaex 7330

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3444  ℩cio 6450  ℩crio 7325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  ordtypelem3  9449  dfac8clem  9961  zorn2lem1  10425  subval  11388  1div0  11813  1div0OLD  11814  divval  11815  elq  12885  flval  13732  ceilval2  13778  cjval  15044  sqrtval  15179  sqrtf  15306  cidval  17618  cidfn  17620  lubdm  18290  lubval  18295  glbdm  18303  glbval  18308  grpinvfval  18892  grpinvval  18894  grpinvfn  18895  pj1val  19609  evlsval  22026  q1pval  26093  ig1pval  26114  coeval  26161  quotval  26233  scutval  27746  dmscut  27757  divsval  28132  mirfv  28636  mirf  28640  usgredg2v  29207  frgrncvvdeqlem5  30282  1div0apr  30447  gidval  30491  grpoinvval  30502  grpoinvf  30511  pjhval  31376  pjfni  31680  cnlnadjlem5  32050  nmopadjlei  32067  cdj3lem2  32414  xdivval  32889  cvmlift3lem4  35302  fvtransport  36013  weiunlem2  36444  finxpreclem4  37375  poimirlem26  37633  lshpkrlem1  39096  lshpkrlem2  39097  lshpkrlem3  39098  trlval  40149  cdleme31fv  40377  cdleme50f  40529  cdlemksv  40831  cdlemkuu  40882  cdlemk40  40904  cdlemk56  40958  cdlemm10N  41105  cdlemn11a  41194  dihval  41219  dihf11lem  41253  dihatlat  41321  dochfl1  41463  mapdhval  41711  hvmapvalvalN  41748  hdmap1vallem  41784  hdmapval  41815  hdmapfnN  41816  hgmapval  41874  hgmapfnN  41875  resubval  42348  redivvald  42423  mpaaval  43133  wessf1ornlem  45172