Theorem riotaex 7401

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2147  Vcvv 3454  ℩cio 6507  ℩crio 7396

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6509  df-riota 7397

This theorem is used by:  ordtypelem3  9538  dfac8clem  10135  zorn2lem1  10598  subval  11572  1div0  11999  divval  12000  elq  13101  flval  13958  ceilval2  14004  cjval  15295  sqrtval  15430  sqrtf  15557  cidval  17877  cidfn  17879  lubdm  18549  lubval  18554  glbdm  18562  glbval  18567  grpinvfval  19215  grpinvval  19217  grpinvfn  19218  pj1val  19936  evlsval  22422  q1pval  26500  ig1pval  26521  coeval  26569  quotval  26640  cutsval  28193  dmcuts  28204  divsval  28602  mirfv  29155  mirf  29159  usgredg2v  29835  frgrncvvdeqlem5  30931  1div0apr  31096  gidval  31141  grpoinvval  31152  grpoinvf  31161  pjhval  32026  pjfni  32330  cnlnadjlem5  32700  nmopadjlei  32717  cdj3lem2  33064  xdivval  33552  cvmlift3lem4  36253  fvtransport  36974  weiunlem  37428  finxpreclem4  38508  poimirlem26  38755  lshpkrlem1  40358  lshpkrlem2  40359  lshpkrlem3  40360  trlval  41410  cdleme31fv  41638  cdleme50f  41790  cdlemksv  42092  cdlemkuu  42143  cdlemk40  42165  cdlemk56  42219  cdlemm10N  42366  cdlemn11a  42455  dihval  42480  dihf11lem  42514  dihatlat  42582  dochfl1  42724  mapdhval  42972  hvmapvalvalN  43009  hdmap1vallem  43045  hdmapval  43076  hdmapfnN  43077  hgmapval  43135  hgmapfnN  43136  resubval  43609  redivvald  43684  mpaaval  44343  wessf1ornlem  46403