Theorem riotaex 7369

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Vcvv 3450  ℩cio 6481  ℩crio 7364

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6483  df-riota 7365

This theorem is used by:  ordtypelem3  9492  dfac8clem  10082  zorn2lem1  10545  subval  11519  1div0  11944  divval  11945  elq  13046  flval  13902  ceilval2  13948  cjval  15236  sqrtval  15371  sqrtf  15498  cidval  17812  cidfn  17814  lubdm  18484  lubval  18489  glbdm  18497  glbval  18502  grpinvfval  19150  grpinvval  19152  grpinvfn  19153  pj1val  19870  evlsval  22356  q1pval  26434  ig1pval  26455  coeval  26503  quotval  26576  cutsval  28099  dmcuts  28110  divsval  28508  mirfv  29061  mirf  29065  usgredg2v  29741  frgrncvvdeqlem5  30837  1div0apr  31002  gidval  31047  grpoinvval  31058  grpoinvf  31067  pjhval  31932  pjfni  32236  cnlnadjlem5  32606  nmopadjlei  32623  cdj3lem2  32970  xdivval  33418  cvmlift3lem4  36008  fvtransport  36719  weiunlem  37173  finxpreclem4  38237  poimirlem26  38484  lshpkrlem1  40087  lshpkrlem2  40088  lshpkrlem3  40089  trlval  41139  cdleme31fv  41367  cdleme50f  41519  cdlemksv  41821  cdlemkuu  41872  cdlemk40  41894  cdlemk56  41948  cdlemm10N  42095  cdlemn11a  42184  dihval  42209  dihf11lem  42243  dihatlat  42311  dochfl1  42453  mapdhval  42701  hvmapvalvalN  42738  hdmap1vallem  42774  hdmapval  42805  hdmapfnN  42806  hgmapval  42864  hgmapfnN  42865  resubval  43346  redivvald  43421  mpaaval  44096  wessf1ornlem  46121