Theorem riotaex 7386

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

Syntax hints:   ∧ wa 394   ∈ wcel 2098  Vcvv 3473  ℩cio 6503  ℩crio 7381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-nul 5310

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-sn 4633  df-pr 4635  df-uni 4913  df-iota 6505  df-riota 7382

This theorem is referenced by:  ordtypelem3  9551  dfac8clem  10063  zorn2lem1  10527  subval  11489  1div0  11911  divval  11912  elq  12972  flval  13799  ceilval2  13845  cjval  15089  sqrtval  15224  sqrtf  15350  cidval  17664  cidfn  17666  lubdm  18350  lubval  18355  glbdm  18363  glbval  18368  grpinvfval  18942  grpinvval  18944  grpinvfn  18945  pj1val  19657  evlsval  22039  q1pval  26110  ig1pval  26130  coeval  26177  quotval  26247  scutval  27753  dmscut  27764  divsval  28109  mirfv  28480  mirf  28484  usgredg2v  29060  frgrncvvdeqlem5  30133  1div0apr  30298  gidval  30342  grpoinvval  30353  grpoinvf  30362  pjhval  31227  pjfni  31531  cnlnadjlem5  31901  nmopadjlei  31918  cdj3lem2  32265  xdivval  32663  cvmlift3lem4  34965  fvtransport  35661  finxpreclem4  36906  poimirlem26  37152  lshpkrlem1  38614  lshpkrlem2  38615  lshpkrlem3  38616  trlval  39667  cdleme31fv  39895  cdleme50f  40047  cdlemksv  40349  cdlemkuu  40400  cdlemk40  40422  cdlemk56  40476  cdlemm10N  40623  cdlemn11a  40712  dihval  40737  dihf11lem  40771  dihatlat  40839  dochfl1  40981  mapdhval  41229  hvmapvalvalN  41266  hdmap1vallem  41302  hdmapval  41333  hdmapfnN  41334  hgmapval  41392  hgmapfnN  41393  resubval  41953  mpaaval  42606  wessf1ornlem  44588