Theorem riotaex 7236

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

Syntax hints:   ∧ wa 396   ∈ wcel 2106  Vcvv 3432  ℩cio 6389  ℩crio 7231

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840  df-iota 6391  df-riota 7232

This theorem is referenced by:  ordtypelem3  9279  dfac8clem  9788  zorn2lem1  10252  subval  11212  1div0  11634  divval  11635  elq  12690  flval  13514  ceilval2  13560  cjval  14813  sqrtval  14948  sqrtf  15075  cidval  17386  cidfn  17388  lubdm  18069  lubval  18074  glbdm  18082  glbval  18087  grpinvfval  18618  grpinvval  18620  grpinvfn  18621  pj1val  19301  evlsval  21296  q1pval  25318  ig1pval  25337  coeval  25384  quotval  25452  mirfv  27017  mirf  27021  usgredg2v  27594  frgrncvvdeqlem5  28667  1div0apr  28832  gidval  28874  grpoinvval  28885  grpoinvf  28894  pjhval  29759  pjfni  30063  cnlnadjlem5  30433  nmopadjlei  30450  cdj3lem2  30797  xdivval  31193  cvmlift3lem4  33284  scutval  33994  dmscut  34005  fvtransport  34334  finxpreclem4  35565  poimirlem26  35803  lshpkrlem1  37124  lshpkrlem2  37125  lshpkrlem3  37126  trlval  38176  cdleme31fv  38404  cdleme50f  38556  cdlemksv  38858  cdlemkuu  38909  cdlemk40  38931  cdlemk56  38985  cdlemm10N  39132  cdlemn11a  39221  dihval  39246  dihf11lem  39280  dihatlat  39348  dochfl1  39490  mapdhval  39738  hvmapvalvalN  39775  hdmap1vallem  39811  hdmapval  39842  hdmapfnN  39843  hgmapval  39901  hgmapfnN  39902  resubval  40350  mpaaval  40976  wessf1ornlem  42722