Theorem riotaex 7325

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Vcvv 3430  ℩cio 6450  ℩crio 7320

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 5242

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 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6452  df-riota 7321

This theorem is referenced by:  ordtypelem3  9432  dfac8clem  9951  zorn2lem1  10415  subval  11381  1div0  11806  1div0OLD  11807  divval  11808  elq  12897  flval  13750  ceilval2  13796  cjval  15061  sqrtval  15196  sqrtf  15323  cidval  17640  cidfn  17642  lubdm  18312  lubval  18317  glbdm  18325  glbval  18330  grpinvfval  18951  grpinvval  18953  grpinvfn  18954  pj1val  19667  evlsval  22080  q1pval  26136  ig1pval  26157  coeval  26204  quotval  26275  cutsval  27792  dmcuts  27803  divsval  28201  mirfv  28744  mirf  28748  usgredg2v  29316  frgrncvvdeqlem5  30394  1div0apr  30559  gidval  30604  grpoinvval  30615  grpoinvf  30624  pjhval  31489  pjfni  31793  cnlnadjlem5  32163  nmopadjlei  32180  cdj3lem2  32527  xdivval  32999  cvmlift3lem4  35526  fvtransport  36236  weiunlem  36667  finxpreclem4  37732  poimirlem26  37989  lshpkrlem1  39578  lshpkrlem2  39579  lshpkrlem3  39580  trlval  40630  cdleme31fv  40858  cdleme50f  41010  cdlemksv  41312  cdlemkuu  41363  cdlemk40  41385  cdlemk56  41439  cdlemm10N  41586  cdlemn11a  41675  dihval  41700  dihf11lem  41734  dihatlat  41802  dochfl1  41944  mapdhval  42192  hvmapvalvalN  42229  hdmap1vallem  42265  hdmapval  42296  hdmapfnN  42297  hgmapval  42355  hgmapfnN  42356  resubval  42821  redivvald  42896  mpaaval  43605  wessf1ornlem  45641