Theorem riotaex 6600

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

Syntax hints:   ∧ wa 384   ∈ wcel 1988  Vcvv 3195  ℩cio 5837  ℩crio 6595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-sn 4169  df-pr 4171  df-uni 4428  df-iota 5839  df-riota 6596

This theorem is referenced by:  ordtypelem3  8410  dfac8clem  8840  zorn2lem1  9303  subval  10257  1div0  10671  divval  10672  elq  11775  flval  12578  ceilval2  12624  cjval  13823  sqrtval  13958  sqrtf  14084  cidval  16319  cidfn  16321  lubdm  16960  lubval  16965  glbdm  16973  glbval  16978  grpinvval  17442  grpinvfn  17443  pj1val  18089  evlsval  19500  q1pval  23894  ig1pval  23913  coeval  23960  quotval  24028  mirfv  25532  mirf  25536  usgredg2v  26100  frgrncvvdeqlem5  27147  1div0apr  27294  gidval  27336  grpoinvval  27347  grpoinvf  27356  pjhval  28226  pjfni  28530  cnlnadjlem5  28900  nmopadjlei  28917  cdj3lem2  29264  xdivval  29601  cvmlift3lem4  31278  scutval  31885  dmscut  31892  fvtransport  32114  finxpreclem4  33202  poimirlem26  33406  lshpkrlem1  34216  lshpkrlem2  34217  lshpkrlem3  34218  trlval  35268  cdleme31fv  35497  cdleme50f  35649  cdlemksv  35951  cdlemkuu  36002  cdlemk40  36024  cdlemk56  36078  cdlemm10N  36226  cdlemn11a  36315  dihval  36340  dihf11lem  36374  dihatlat  36442  dochfl1  36584  mapdhval  36832  hvmapvalvalN  36869  hdmap1vallem  36906  hdmapval  36939  hdmapfnN  36940  hgmapval  36998  hgmapfnN  36999  mpaaval  37540  wessf1ornlem  39187