Theorem riotaex 7348

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3447  ℩cio 6462  ℩crio 7343

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 5261

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 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-riota 7344

This theorem is referenced by:  ordtypelem3  9473  dfac8clem  9985  zorn2lem1  10449  subval  11412  1div0  11837  1div0OLD  11838  divval  11839  elq  12909  flval  13756  ceilval2  13802  cjval  15068  sqrtval  15203  sqrtf  15330  cidval  17638  cidfn  17640  lubdm  18310  lubval  18315  glbdm  18323  glbval  18328  grpinvfval  18910  grpinvval  18912  grpinvfn  18913  pj1val  19625  evlsval  21993  q1pval  26060  ig1pval  26081  coeval  26128  quotval  26200  scutval  27712  dmscut  27723  divsval  28092  mirfv  28583  mirf  28587  usgredg2v  29154  frgrncvvdeqlem5  30232  1div0apr  30397  gidval  30441  grpoinvval  30452  grpoinvf  30461  pjhval  31326  pjfni  31630  cnlnadjlem5  32000  nmopadjlei  32017  cdj3lem2  32364  xdivval  32839  cvmlift3lem4  35309  fvtransport  36020  weiunlem2  36451  finxpreclem4  37382  poimirlem26  37640  lshpkrlem1  39103  lshpkrlem2  39104  lshpkrlem3  39105  trlval  40156  cdleme31fv  40384  cdleme50f  40536  cdlemksv  40838  cdlemkuu  40889  cdlemk40  40911  cdlemk56  40965  cdlemm10N  41112  cdlemn11a  41201  dihval  41226  dihf11lem  41260  dihatlat  41328  dochfl1  41470  mapdhval  41718  hvmapvalvalN  41755  hdmap1vallem  41791  hdmapval  41822  hdmapfnN  41823  hgmapval  41881  hgmapfnN  41882  resubval  42355  redivvald  42430  mpaaval  43140  wessf1ornlem  45179