Theorem riotaex 7381

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144  Vcvv 3450  ℩cio 6492  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  ordtypelem3  9514  dfac8clem  10111  zorn2lem1  10574  subval  11548  1div0  11975  divval  11976  elq  13077  flval  13934  ceilval2  13980  cjval  15269  sqrtval  15404  sqrtf  15531  cidval  17851  cidfn  17853  lubdm  18523  lubval  18528  glbdm  18536  glbval  18541  grpinvfval  19189  grpinvval  19191  grpinvfn  19192  pj1val  19909  evlsval  22395  q1pval  26473  ig1pval  26494  coeval  26542  quotval  26613  cutsval  28166  dmcuts  28177  divsval  28575  mirfv  29128  mirf  29132  usgredg2v  29808  frgrncvvdeqlem5  30904  1div0apr  31069  gidval  31114  grpoinvval  31125  grpoinvf  31134  pjhval  31999  pjfni  32303  cnlnadjlem5  32673  nmopadjlei  32690  cdj3lem2  33037  xdivval  33485  cvmlift3lem4  36087  fvtransport  36797  weiunlem  37251  finxpreclem4  38318  poimirlem26  38565  lshpkrlem1  40168  lshpkrlem2  40169  lshpkrlem3  40170  trlval  41220  cdleme31fv  41448  cdleme50f  41600  cdlemksv  41902  cdlemkuu  41953  cdlemk40  41975  cdlemk56  42029  cdlemm10N  42176  cdlemn11a  42265  dihval  42290  dihf11lem  42324  dihatlat  42392  dochfl1  42534  mapdhval  42782  hvmapvalvalN  42819  hdmap1vallem  42855  hdmapval  42886  hdmapfnN  42887  hgmapval  42945  hgmapfnN  42946  resubval  43419  redivvald  43494  mpaaval  44153  wessf1ornlem  46200