Theorem riotaex 7408

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Vcvv 3488  ℩cio 6523  ℩crio 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-riota 7404

This theorem is referenced by:  ordtypelem3  9589  dfac8clem  10101  zorn2lem1  10565  subval  11527  1div0  11949  1div0OLD  11950  divval  11951  elq  13015  flval  13845  ceilval2  13891  cjval  15151  sqrtval  15286  sqrtf  15412  cidval  17735  cidfn  17737  lubdm  18421  lubval  18426  glbdm  18434  glbval  18439  grpinvfval  19018  grpinvval  19020  grpinvfn  19021  pj1val  19737  evlsval  22133  q1pval  26214  ig1pval  26235  coeval  26282  quotval  26352  scutval  27863  dmscut  27874  divsval  28233  mirfv  28682  mirf  28686  usgredg2v  29262  frgrncvvdeqlem5  30335  1div0apr  30500  gidval  30544  grpoinvval  30555  grpoinvf  30564  pjhval  31429  pjfni  31733  cnlnadjlem5  32103  nmopadjlei  32120  cdj3lem2  32467  xdivval  32883  cvmlift3lem4  35290  fvtransport  35996  weiunlem2  36429  finxpreclem4  37360  poimirlem26  37606  lshpkrlem1  39066  lshpkrlem2  39067  lshpkrlem3  39068  trlval  40119  cdleme31fv  40347  cdleme50f  40499  cdlemksv  40801  cdlemkuu  40852  cdlemk40  40874  cdlemk56  40928  cdlemm10N  41075  cdlemn11a  41164  dihval  41189  dihf11lem  41223  dihatlat  41291  dochfl1  41433  mapdhval  41681  hvmapvalvalN  41718  hdmap1vallem  41754  hdmapval  41785  hdmapfnN  41786  hgmapval  41844  hgmapfnN  41845  resubval  42343  mpaaval  43108  wessf1ornlem  45092