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 6469	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V
3	1, 2	eqeltri 2833	1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3441  ℩cio 6447  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5252

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-sn 4582  df-pr 4584  df-uni 4865  df-iota 6449  df-riota 7317

This theorem is referenced by:  ordtypelem3  9429  dfac8clem  9946  zorn2lem1  10410  subval  11375  1div0  11800  1div0OLD  11801  divval  11802  elq  12867  flval  13718  ceilval2  13764  cjval  15029  sqrtval  15164  sqrtf  15291  cidval  17604  cidfn  17606  lubdm  18276  lubval  18281  glbdm  18289  glbval  18294  grpinvfval  18912  grpinvval  18914  grpinvfn  18915  pj1val  19628  evlsval  22045  q1pval  26120  ig1pval  26141  coeval  26188  quotval  26260  cutsval  27780  dmcuts  27791  divsval  28189  mirfv  28732  mirf  28736  usgredg2v  29304  frgrncvvdeqlem5  30382  1div0apr  30547  gidval  30591  grpoinvval  30602  grpoinvf  30611  pjhval  31476  pjfni  31780  cnlnadjlem5  32150  nmopadjlei  32167  cdj3lem2  32514  xdivval  33002  cvmlift3lem4  35518  fvtransport  36228  weiunlem  36659  finxpreclem4  37601  poimirlem26  37849  lshpkrlem1  39438  lshpkrlem2  39439  lshpkrlem3  39440  trlval  40490  cdleme31fv  40718  cdleme50f  40870  cdlemksv  41172  cdlemkuu  41223  cdlemk40  41245  cdlemk56  41299  cdlemm10N  41446  cdlemn11a  41535  dihval  41560  dihf11lem  41594  dihatlat  41662  dochfl1  41804  mapdhval  42052  hvmapvalvalN  42089  hdmap1vallem  42125  hdmapval  42156  hdmapfnN  42157  hgmapval  42215  hgmapfnN  42216  resubval  42689  redivvald  42764  mpaaval  43460  wessf1ornlem  45496