Theorem riotaex 7392

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

Syntax hints:   ∧ wa 395   ∈ wcel 2106  Vcvv 3478  ℩cio 6514  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-sn 4632  df-pr 4634  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  ordtypelem3  9558  dfac8clem  10070  zorn2lem1  10534  subval  11497  1div0  11920  1div0OLD  11921  divval  11922  elq  12990  flval  13831  ceilval2  13877  cjval  15138  sqrtval  15273  sqrtf  15399  cidval  17722  cidfn  17724  lubdm  18409  lubval  18414  glbdm  18422  glbval  18427  grpinvfval  19009  grpinvval  19011  grpinvfn  19012  pj1val  19728  evlsval  22128  q1pval  26209  ig1pval  26230  coeval  26277  quotval  26349  scutval  27860  dmscut  27871  divsval  28230  mirfv  28679  mirf  28683  usgredg2v  29259  frgrncvvdeqlem5  30332  1div0apr  30497  gidval  30541  grpoinvval  30552  grpoinvf  30561  pjhval  31426  pjfni  31730  cnlnadjlem5  32100  nmopadjlei  32117  cdj3lem2  32464  xdivval  32886  cvmlift3lem4  35307  fvtransport  36014  weiunlem2  36446  finxpreclem4  37377  poimirlem26  37633  lshpkrlem1  39092  lshpkrlem2  39093  lshpkrlem3  39094  trlval  40145  cdleme31fv  40373  cdleme50f  40525  cdlemksv  40827  cdlemkuu  40878  cdlemk40  40900  cdlemk56  40954  cdlemm10N  41101  cdlemn11a  41190  dihval  41215  dihf11lem  41249  dihatlat  41317  dochfl1  41459  mapdhval  41707  hvmapvalvalN  41744  hdmap1vallem  41780  hdmapval  41811  hdmapfnN  41812  hgmapval  41870  hgmapfnN  41871  resubval  42374  mpaaval  43140  wessf1ornlem  45128