Theorem riotaex 7328

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3429  ℩cio 6452  ℩crio 7323

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 2708  ax-nul 5241

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-riota 7324

This theorem is referenced by:  ordtypelem3  9435  dfac8clem  9954  zorn2lem1  10418  subval  11384  1div0  11809  1div0OLD  11810  divval  11811  elq  12900  flval  13753  ceilval2  13799  cjval  15064  sqrtval  15199  sqrtf  15326  cidval  17643  cidfn  17645  lubdm  18315  lubval  18320  glbdm  18328  glbval  18333  grpinvfval  18954  grpinvval  18956  grpinvfn  18957  pj1val  19670  evlsval  22064  q1pval  26120  ig1pval  26141  coeval  26188  quotval  26258  cutsval  27772  dmcuts  27783  divsval  28181  mirfv  28724  mirf  28728  usgredg2v  29296  frgrncvvdeqlem5  30373  1div0apr  30538  gidval  30583  grpoinvval  30594  grpoinvf  30603  pjhval  31468  pjfni  31772  cnlnadjlem5  32142  nmopadjlei  32159  cdj3lem2  32506  xdivval  32978  cvmlift3lem4  35504  fvtransport  36214  weiunlem  36645  finxpreclem4  37710  poimirlem26  37967  lshpkrlem1  39556  lshpkrlem2  39557  lshpkrlem3  39558  trlval  40608  cdleme31fv  40836  cdleme50f  40988  cdlemksv  41290  cdlemkuu  41341  cdlemk40  41363  cdlemk56  41417  cdlemm10N  41564  cdlemn11a  41653  dihval  41678  dihf11lem  41712  dihatlat  41780  dochfl1  41922  mapdhval  42170  hvmapvalvalN  42207  hdmap1vallem  42243  hdmapval  42274  hdmapfnN  42275  hgmapval  42333  hgmapfnN  42334  resubval  42799  redivvald  42874  mpaaval  43579  wessf1ornlem  45615