Theorem riotaex 6870

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

Syntax hints:   ∧ wa 386   ∈ wcel 2164  Vcvv 3414  ℩cio 6084  ℩crio 6865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-nul 5013

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-sn 4398  df-pr 4400  df-uni 4659  df-iota 6086  df-riota 6866

This theorem is referenced by:  ordtypelem3  8694  dfac8clem  9168  zorn2lem1  9633  subval  10592  1div0  11011  divval  11012  elq  12073  flval  12890  ceilval2  12936  cjval  14219  sqrtval  14354  sqrtf  14480  cidval  16690  cidfn  16692  lubdm  17332  lubval  17337  glbdm  17345  glbval  17350  grpinvval  17815  grpinvfn  17816  pj1val  18459  evlsval  19879  q1pval  24312  ig1pval  24331  coeval  24378  quotval  24446  mirfv  25968  mirf  25972  usgredg2v  26523  frgrncvvdeqlem5  27673  1div0apr  27871  gidval  27911  grpoinvval  27922  grpoinvf  27931  pjhval  28800  pjfni  29104  cnlnadjlem5  29474  nmopadjlei  29491  cdj3lem2  29838  xdivval  30161  cvmlift3lem4  31839  scutval  32439  dmscut  32446  fvtransport  32667  finxpreclem4  33769  poimirlem26  33972  lshpkrlem1  35178  lshpkrlem2  35179  lshpkrlem3  35180  trlval  36230  cdleme31fv  36458  cdleme50f  36610  cdlemksv  36912  cdlemkuu  36963  cdlemk40  36985  cdlemk56  37039  cdlemm10N  37186  cdlemn11a  37275  dihval  37300  dihf11lem  37334  dihatlat  37402  dochfl1  37544  mapdhval  37792  hvmapvalvalN  37829  hdmap1vallem  37865  hdmapval  37896  hdmapfnN  37897  hgmapval  37955  hgmapfnN  37956  resubval  38064  mpaaval  38557  wessf1ornlem  40172