Theorem riotaex 7375

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

Syntax hints:   ∧ wa 400   ∈ wcel 2150  Vcvv 3462  ℩cio 6494  ℩crio 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-nul 5274

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ne 2966  df-v 3464  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-sn 4595  df-pr 4597  df-uni 4878  df-iota 6496  df-riota 7371

This theorem is referenced by:  ordtypelem3  9485  dfac8clem  10019  zorn2lem1  10483  subval  11451  1div0  11876  divval  11877  elq  12977  flval  13830  ceilval2  13876  cjval  15156  sqrtval  15291  sqrtf  15418  cidval  17736  cidfn  17738  lubdm  18408  lubval  18413  glbdm  18421  glbval  18426  grpinvfval  19048  grpinvval  19050  grpinvfn  19051  pj1val  19768  evlsval  22220  q1pval  26295  ig1pval  26316  coeval  26363  quotval  26436  cutsval  27953  dmcuts  27964  divsval  28362  mirfv  28913  mirf  28917  usgredg2v  29547  frgrncvvdeqlem5  30624  1div0apr  30789  gidval  30834  grpoinvval  30845  grpoinvf  30854  pjhval  31719  pjfni  32023  cnlnadjlem5  32393  nmopadjlei  32410  cdj3lem2  32757  xdivval  33208  cvmlift3lem4  35772  fvtransport  36482  weiunlem  36922  finxpreclem4  37988  poimirlem26  38245  lshpkrlem1  39834  lshpkrlem2  39835  lshpkrlem3  39836  trlval  40886  cdleme31fv  41114  cdleme50f  41266  cdlemksv  41568  cdlemkuu  41619  cdlemk40  41641  cdlemk56  41695  cdlemm10N  41842  cdlemn11a  41931  dihval  41956  dihf11lem  41990  dihatlat  42058  dochfl1  42200  mapdhval  42448  hvmapvalvalN  42485  hdmap1vallem  42521  hdmapval  42552  hdmapfnN  42553  hgmapval  42611  hgmapfnN  42612  resubval  43078  redivvald  43153  mpaaval  43830  wessf1ornlem  45855