Theorem riotaex 7366

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

Syntax hints:   ∧ wa 397   ∈ wcel 2107  Vcvv 3475  ℩cio 6491  ℩crio 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6493  df-riota 7362

This theorem is referenced by:  ordtypelem3  9512  dfac8clem  10024  zorn2lem1  10488  subval  11448  1div0  11870  divval  11871  elq  12931  flval  13756  ceilval2  13802  cjval  15046  sqrtval  15181  sqrtf  15307  cidval  17618  cidfn  17620  lubdm  18301  lubval  18306  glbdm  18314  glbval  18319  grpinvfval  18860  grpinvval  18862  grpinvfn  18863  pj1val  19558  evlsval  21641  q1pval  25663  ig1pval  25682  coeval  25729  quotval  25797  scutval  27291  dmscut  27302  divsval  27627  mirfv  27897  mirf  27901  usgredg2v  28474  frgrncvvdeqlem5  29546  1div0apr  29711  gidval  29753  grpoinvval  29764  grpoinvf  29773  pjhval  30638  pjfni  30942  cnlnadjlem5  31312  nmopadjlei  31329  cdj3lem2  31676  xdivval  32073  cvmlift3lem4  34302  fvtransport  34993  finxpreclem4  36264  poimirlem26  36503  lshpkrlem1  37969  lshpkrlem2  37970  lshpkrlem3  37971  trlval  39022  cdleme31fv  39250  cdleme50f  39402  cdlemksv  39704  cdlemkuu  39755  cdlemk40  39777  cdlemk56  39831  cdlemm10N  39978  cdlemn11a  40067  dihval  40092  dihf11lem  40126  dihatlat  40194  dochfl1  40336  mapdhval  40584  hvmapvalvalN  40621  hdmap1vallem  40657  hdmapval  40688  hdmapfnN  40689  hgmapval  40747  hgmapfnN  40748  resubval  41237  mpaaval  41879  wessf1ornlem  43868