Theorem riotaex 7371

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3464  ℩cio 6487  ℩crio 7366

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

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-sn 4607  df-pr 4609  df-uni 4889  df-iota 6489  df-riota 7367

This theorem is referenced by:  ordtypelem3  9539  dfac8clem  10051  zorn2lem1  10515  subval  11478  1div0  11901  1div0OLD  11902  divval  11903  elq  12971  flval  13816  ceilval2  13862  cjval  15126  sqrtval  15261  sqrtf  15387  cidval  17694  cidfn  17696  lubdm  18366  lubval  18371  glbdm  18379  glbval  18384  grpinvfval  18966  grpinvval  18968  grpinvfn  18969  pj1val  19681  evlsval  22049  q1pval  26117  ig1pval  26138  coeval  26185  quotval  26257  scutval  27769  dmscut  27780  divsval  28149  mirfv  28640  mirf  28644  usgredg2v  29211  frgrncvvdeqlem5  30289  1div0apr  30454  gidval  30498  grpoinvval  30509  grpoinvf  30518  pjhval  31383  pjfni  31687  cnlnadjlem5  32057  nmopadjlei  32074  cdj3lem2  32421  xdivval  32898  cvmlift3lem4  35349  fvtransport  36055  weiunlem2  36486  finxpreclem4  37417  poimirlem26  37675  lshpkrlem1  39133  lshpkrlem2  39134  lshpkrlem3  39135  trlval  40186  cdleme31fv  40414  cdleme50f  40566  cdlemksv  40868  cdlemkuu  40919  cdlemk40  40941  cdlemk56  40995  cdlemm10N  41142  cdlemn11a  41231  dihval  41256  dihf11lem  41290  dihatlat  41358  dochfl1  41500  mapdhval  41748  hvmapvalvalN  41785  hdmap1vallem  41821  hdmapval  41852  hdmapfnN  41853  hgmapval  41911  hgmapfnN  41912  resubval  42377  mpaaval  43142  wessf1ornlem  45176