Theorem riotaex 7125

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

Syntax hints:   ∧ wa 399   ∈ wcel 2113  Vcvv 3397  ℩cio 6289  ℩crio 7120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-nul 5171

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-sn 4514  df-pr 4516  df-uni 4794  df-iota 6291  df-riota 7121

This theorem is referenced by:  ordtypelem3  9050  dfac8clem  9525  zorn2lem1  9989  subval  10948  1div0  11370  divval  11371  elq  12425  flval  13248  ceilval2  13294  cjval  14544  sqrtval  14679  sqrtf  14806  cidval  17044  cidfn  17046  lubdm  17698  lubval  17703  glbdm  17711  glbval  17716  grpinvfval  18253  grpinvval  18255  grpinvfn  18256  pj1val  18932  evlsval  20893  q1pval  24898  ig1pval  24917  coeval  24964  quotval  25032  mirfv  26594  mirf  26598  usgredg2v  27161  frgrncvvdeqlem5  28232  1div0apr  28397  gidval  28439  grpoinvval  28450  grpoinvf  28459  pjhval  29324  pjfni  29628  cnlnadjlem5  29998  nmopadjlei  30015  cdj3lem2  30362  xdivval  30760  cvmlift3lem4  32847  scutval  33627  dmscut  33638  fvtransport  33964  finxpreclem4  35177  poimirlem26  35415  lshpkrlem1  36736  lshpkrlem2  36737  lshpkrlem3  36738  trlval  37788  cdleme31fv  38016  cdleme50f  38168  cdlemksv  38470  cdlemkuu  38521  cdlemk40  38543  cdlemk56  38597  cdlemm10N  38744  cdlemn11a  38833  dihval  38858  dihf11lem  38892  dihatlat  38960  dochfl1  39102  mapdhval  39350  hvmapvalvalN  39387  hdmap1vallem  39423  hdmapval  39454  hdmapfnN  39455  hgmapval  39513  hgmapfnN  39514  resubval  39911  mpaaval  40532  wessf1ornlem  42244