Theorem riotaex 7330

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3444  ℩cio 6450  ℩crio 7325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  ordtypelem3  9449  dfac8clem  9963  zorn2lem1  10427  subval  11390  1div0  11815  1div0OLD  11816  divval  11817  elq  12887  flval  13734  ceilval2  13780  cjval  15045  sqrtval  15180  sqrtf  15307  cidval  17619  cidfn  17621  lubdm  18291  lubval  18296  glbdm  18304  glbval  18309  grpinvfval  18893  grpinvval  18895  grpinvfn  18896  pj1val  19610  evlsval  22027  q1pval  26094  ig1pval  26115  coeval  26162  quotval  26234  scutval  27747  dmscut  27758  divsval  28133  mirfv  28637  mirf  28641  usgredg2v  29208  frgrncvvdeqlem5  30283  1div0apr  30448  gidval  30492  grpoinvval  30503  grpoinvf  30512  pjhval  31377  pjfni  31681  cnlnadjlem5  32051  nmopadjlei  32068  cdj3lem2  32415  xdivval  32890  cvmlift3lem4  35303  fvtransport  36014  weiunlem2  36445  finxpreclem4  37376  poimirlem26  37634  lshpkrlem1  39097  lshpkrlem2  39098  lshpkrlem3  39099  trlval  40150  cdleme31fv  40378  cdleme50f  40530  cdlemksv  40832  cdlemkuu  40883  cdlemk40  40905  cdlemk56  40959  cdlemm10N  41106  cdlemn11a  41195  dihval  41220  dihf11lem  41254  dihatlat  41322  dochfl1  41464  mapdhval  41712  hvmapvalvalN  41749  hdmap1vallem  41785  hdmapval  41816  hdmapfnN  41817  hgmapval  41875  hgmapfnN  41876  resubval  42349  redivvald  42424  mpaaval  43134  wessf1ornlem  45173