Theorem riotaex 6757

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

Syntax hints:   ∧ wa 382   ∈ wcel 2144  Vcvv 3349  ℩cio 5992  ℩crio 6752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-nul 4920

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-sn 4315  df-pr 4317  df-uni 4573  df-iota 5994  df-riota 6753

This theorem is referenced by:  ordtypelem3  8580  dfac8clem  9054  zorn2lem1  9519  subval  10473  1div0  10887  divval  10888  elq  11992  flval  12802  ceilval2  12848  cjval  14049  sqrtval  14184  sqrtf  14310  cidval  16544  cidfn  16546  lubdm  17186  lubval  17191  glbdm  17199  glbval  17204  grpinvval  17668  grpinvfn  17669  pj1val  18314  evlsval  19733  q1pval  24132  ig1pval  24151  coeval  24198  quotval  24266  mirfv  25771  mirf  25775  usgredg2v  26340  frgrncvvdeqlem5  27482  1div0apr  27660  gidval  27700  grpoinvval  27711  grpoinvf  27720  pjhval  28590  pjfni  28894  cnlnadjlem5  29264  nmopadjlei  29281  cdj3lem2  29628  xdivval  29961  cvmlift3lem4  31636  scutval  32242  dmscut  32249  fvtransport  32470  finxpreclem4  33561  poimirlem26  33761  lshpkrlem1  34912  lshpkrlem2  34913  lshpkrlem3  34914  trlval  35964  cdleme31fv  36192  cdleme50f  36344  cdlemksv  36646  cdlemkuu  36697  cdlemk40  36719  cdlemk56  36773  cdlemm10N  36921  cdlemn11a  37010  dihval  37035  dihf11lem  37069  dihatlat  37137  dochfl1  37279  mapdhval  37527  hvmapvalvalN  37564  hdmap1vallem  37600  hdmapval  37631  hdmapfnN  37632  hgmapval  37690  hgmapfnN  37691  mpaaval  38240  wessf1ornlem  39885