Theorem riotaex 7377

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Vcvv 3453  ℩cio 6491  ℩crio 7372

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493  df-riota 7373

This theorem is used by:  ordtypelem3  9495  dfac8clem  10038  zorn2lem1  10501  subval  11475  1div0  11900  divval  11901  elq  13002  flval  13857  ceilval2  13903  cjval  15191  sqrtval  15326  sqrtf  15453  cidval  17769  cidfn  17771  lubdm  18441  lubval  18446  glbdm  18454  glbval  18459  grpinvfval  19103  grpinvval  19105  grpinvfn  19106  pj1val  19823  evlsval  22303  q1pval  26382  ig1pval  26403  coeval  26450  quotval  26523  cutsval  28043  dmcuts  28054  divsval  28452  mirfv  29005  mirf  29009  usgredg2v  29673  frgrncvvdeqlem5  30769  1div0apr  30934  gidval  30979  grpoinvval  30990  grpoinvf  30999  pjhval  31864  pjfni  32168  cnlnadjlem5  32538  nmopadjlei  32555  cdj3lem2  32902  xdivval  33351  cvmlift3lem4  35888  fvtransport  36599  weiunlem  37069  finxpreclem4  38135  poimirlem26  38382  lshpkrlem1  39970  lshpkrlem2  39971  lshpkrlem3  39972  trlval  41022  cdleme31fv  41250  cdleme50f  41402  cdlemksv  41704  cdlemkuu  41755  cdlemk40  41777  cdlemk56  41831  cdlemm10N  41978  cdlemn11a  42067  dihval  42092  dihf11lem  42126  dihatlat  42194  dochfl1  42336  mapdhval  42584  hvmapvalvalN  42621  hdmap1vallem  42657  hdmapval  42688  hdmapfnN  42689  hgmapval  42747  hgmapfnN  42748  resubval  43229  redivvald  43304  mpaaval  43979  wessf1ornlem  46004