Theorem riotaex 7393

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

Syntax hints:   ∧ wa 395   ∈ wcel 2107  Vcvv 3479  ℩cio 6511  ℩crio 7388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-sn 4626  df-pr 4628  df-uni 4907  df-iota 6513  df-riota 7389

This theorem is referenced by:  ordtypelem3  9561  dfac8clem  10073  zorn2lem1  10537  subval  11500  1div0  11923  1div0OLD  11924  divval  11925  elq  12993  flval  13835  ceilval2  13881  cjval  15142  sqrtval  15277  sqrtf  15403  cidval  17721  cidfn  17723  lubdm  18397  lubval  18402  glbdm  18410  glbval  18415  grpinvfval  18997  grpinvval  18999  grpinvfn  19000  pj1val  19714  evlsval  22111  q1pval  26195  ig1pval  26216  coeval  26263  quotval  26335  scutval  27846  dmscut  27857  divsval  28216  mirfv  28665  mirf  28669  usgredg2v  29245  frgrncvvdeqlem5  30323  1div0apr  30488  gidval  30532  grpoinvval  30543  grpoinvf  30552  pjhval  31417  pjfni  31721  cnlnadjlem5  32091  nmopadjlei  32108  cdj3lem2  32455  xdivval  32902  cvmlift3lem4  35328  fvtransport  36034  weiunlem2  36465  finxpreclem4  37396  poimirlem26  37654  lshpkrlem1  39112  lshpkrlem2  39113  lshpkrlem3  39114  trlval  40165  cdleme31fv  40393  cdleme50f  40545  cdlemksv  40847  cdlemkuu  40898  cdlemk40  40920  cdlemk56  40974  cdlemm10N  41121  cdlemn11a  41210  dihval  41235  dihf11lem  41269  dihatlat  41337  dochfl1  41479  mapdhval  41727  hvmapvalvalN  41764  hdmap1vallem  41800  hdmapval  41831  hdmapfnN  41832  hgmapval  41890  hgmapfnN  41891  resubval  42402  mpaaval  43168  wessf1ornlem  45195