Theorem riotaex 7373

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

This proof depends on syntax axioms:   ∧ wa 400   ∈ wcel 2142  Vcvv 3454  ℩cio 6490  ℩crio 7368

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-sn 4589  df-pr 4591  df-uni 4872  df-iota 6492  df-riota 7369

This theorem is used by:  ordtypelem3  9480  dfac8clem  10023  zorn2lem1  10486  subval  11454  1div0  11879  divval  11880  elq  12980  flval  13834  ceilval2  13880  cjval  15160  sqrtval  15295  sqrtf  15422  cidval  17739  cidfn  17741  lubdm  18411  lubval  18416  glbdm  18424  glbval  18429  grpinvfval  19051  grpinvval  19053  grpinvfn  19054  pj1val  19771  evlsval  22248  q1pval  26323  ig1pval  26344  coeval  26391  quotval  26464  cutsval  27984  dmcuts  27995  divsval  28393  mirfv  28944  mirf  28948  usgredg2v  29588  frgrncvvdeqlem5  30665  1div0apr  30830  gidval  30875  grpoinvval  30886  grpoinvf  30895  pjhval  31760  pjfni  32064  cnlnadjlem5  32434  nmopadjlei  32451  cdj3lem2  32798  xdivval  33249  cvmlift3lem4  35822  fvtransport  36532  weiunlem  37002  finxpreclem4  38068  poimirlem26  38325  lshpkrlem1  39912  lshpkrlem2  39913  lshpkrlem3  39914  trlval  40964  cdleme31fv  41192  cdleme50f  41344  cdlemksv  41646  cdlemkuu  41697  cdlemk40  41719  cdlemk56  41773  cdlemm10N  41920  cdlemn11a  42009  dihval  42034  dihf11lem  42068  dihatlat  42136  dochfl1  42278  mapdhval  42526  hvmapvalvalN  42563  hdmap1vallem  42599  hdmapval  42630  hdmapfnN  42631  hgmapval  42689  hgmapfnN  42690  resubval  43156  redivvald  43231  mpaaval  43906  wessf1ornlem  45931