Theorem riotaex 6515

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

Syntax hints:   ∧ wa 383   ∈ wcel 1977  Vcvv 3173  ℩cio 5766  ℩crio 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-riota 6511

This theorem is referenced by:  ordtypelem3  8308  dfac8clem  8738  zorn2lem1  9201  subval  10151  1div0  10565  divval  10566  elq  11666  flval  12457  ceilval2  12503  cjval  13690  sqrtval  13825  sqrtf  13951  cidval  16161  cidfn  16163  lubdm  16802  lubval  16807  glbdm  16815  glbval  16820  grpinvval  17284  grpinvfn  17285  pj1val  17931  evlsval  19340  q1pval  23717  ig1pval  23736  coeval  23783  quotval  23851  mirfv  25351  mirf  25355  usgraidx2v  25922  nbgraf1olem4  25973  frgrancvvdeqlem6  26562  1div0apr  26716  gidval  26750  grpoinvval  26761  grpoinvf  26770  pjhval  27640  pjfni  27944  cnlnadjlem5  28314  nmopadjlei  28331  cdj3lem2  28678  xdivval  28958  cvmlift3lem4  30558  fvtransport  31309  finxpreclem4  32407  poimirlem26  32605  lshpkrlem1  33415  lshpkrlem2  33416  lshpkrlem3  33417  trlval  34467  cdleme31fv  34696  cdleme50f  34848  cdlemksv  35150  cdlemkuu  35201  cdlemk40  35223  cdlemk56  35277  cdlemm10N  35425  cdlemn11a  35514  dihval  35539  dihf11lem  35573  dihatlat  35641  dochfl1  35783  mapdhval  36031  hvmapvalvalN  36068  hdmap1vallem  36105  hdmapval  36138  hdmapfnN  36139  hgmapval  36197  hgmapfnN  36198  mpaaval  36740  wessf1ornlem  38366  usgredg2v  40454  frgrncvvdeqlem6  41474