Theorem riotaex 7321

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

Syntax hints:   ∧ wa 397   ∈ wcel 2121  Vcvv 3433  ℩cio 6443  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-sn 4559  df-pr 4561  df-uni 4842  df-iota 6445  df-riota 7317

This theorem is referenced by:  ordtypelem3  9429  dfac8clem  9949  zorn2lem1  10413  subval  11379  1div0  11804  1div0OLD  11805  divval  11806  elq  12895  flval  13748  ceilval2  13794  cjval  15059  sqrtval  15194  sqrtf  15321  cidval  17638  cidfn  17640  lubdm  18310  lubval  18315  glbdm  18323  glbval  18328  grpinvfval  18949  grpinvval  18951  grpinvfn  18952  pj1val  19665  evlsval  22066  q1pval  26142  ig1pval  26163  coeval  26210  quotval  26280  cutsval  27794  dmcuts  27805  divsval  28203  mirfv  28746  mirf  28750  usgredg2v  29318  frgrncvvdeqlem5  30395  1div0apr  30560  gidval  30605  grpoinvval  30616  grpoinvf  30625  pjhval  31490  pjfni  31794  cnlnadjlem5  32164  nmopadjlei  32181  cdj3lem2  32528  xdivval  33001  cvmlift3lem4  35565  fvtransport  36275  weiunlem  36706  finxpreclem4  37771  poimirlem26  38028  lshpkrlem1  39617  lshpkrlem2  39618  lshpkrlem3  39619  trlval  40669  cdleme31fv  40897  cdleme50f  41049  cdlemksv  41351  cdlemkuu  41402  cdlemk40  41424  cdlemk56  41478  cdlemm10N  41625  cdlemn11a  41714  dihval  41739  dihf11lem  41773  dihatlat  41841  dochfl1  41983  mapdhval  42231  hvmapvalvalN  42268  hdmap1vallem  42304  hdmapval  42335  hdmapfnN  42336  hgmapval  42394  hgmapfnN  42395  resubval  42859  redivvald  42934  mpaaval  43611  wessf1ornlem  45646