Theorem riotaex 7097

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

Syntax hints:   ∧ wa 399   ∈ wcel 2111  Vcvv 3441  ℩cio 6281  ℩crio 7092

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-uni 4801  df-iota 6283  df-riota 7093

This theorem is referenced by:  ordtypelem3  8968  dfac8clem  9443  zorn2lem1  9907  subval  10866  1div0  11288  divval  11289  elq  12338  flval  13159  ceilval2  13205  cjval  14453  sqrtval  14588  sqrtf  14715  cidval  16940  cidfn  16942  lubdm  17581  lubval  17586  glbdm  17594  glbval  17599  grpinvfval  18134  grpinvval  18136  grpinvfn  18137  pj1val  18813  evlsval  20758  q1pval  24754  ig1pval  24773  coeval  24820  quotval  24888  mirfv  26450  mirf  26454  usgredg2v  27017  frgrncvvdeqlem5  28088  1div0apr  28253  gidval  28295  grpoinvval  28306  grpoinvf  28315  pjhval  29180  pjfni  29484  cnlnadjlem5  29854  nmopadjlei  29871  cdj3lem2  30218  xdivval  30621  cvmlift3lem4  32682  scutval  33378  dmscut  33385  fvtransport  33606  finxpreclem4  34811  poimirlem26  35083  lshpkrlem1  36406  lshpkrlem2  36407  lshpkrlem3  36408  trlval  37458  cdleme31fv  37686  cdleme50f  37838  cdlemksv  38140  cdlemkuu  38191  cdlemk40  38213  cdlemk56  38267  cdlemm10N  38414  cdlemn11a  38503  dihval  38528  dihf11lem  38562  dihatlat  38630  dochfl1  38772  mapdhval  39020  hvmapvalvalN  39057  hdmap1vallem  39093  hdmapval  39124  hdmapfnN  39125  hgmapval  39183  hgmapfnN  39184  resubval  39505  mpaaval  40095  wessf1ornlem  41811