Theorem riotaex 7118

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

Syntax hints:   ∧ wa 398   ∈ wcel 2114  Vcvv 3494  ℩cio 6312  ℩crio 7113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4568  df-pr 4570  df-uni 4839  df-iota 6314  df-riota 7114

This theorem is referenced by:  ordtypelem3  8984  dfac8clem  9458  zorn2lem1  9918  subval  10877  1div0  11299  divval  11300  elq  12351  flval  13165  ceilval2  13211  cjval  14461  sqrtval  14596  sqrtf  14723  cidval  16948  cidfn  16950  lubdm  17589  lubval  17594  glbdm  17602  glbval  17607  grpinvfval  18142  grpinvval  18144  grpinvfn  18145  pj1val  18821  evlsval  20299  q1pval  24747  ig1pval  24766  coeval  24813  quotval  24881  mirfv  26442  mirf  26446  usgredg2v  27009  frgrncvvdeqlem5  28082  1div0apr  28247  gidval  28289  grpoinvval  28300  grpoinvf  28309  pjhval  29174  pjfni  29478  cnlnadjlem5  29848  nmopadjlei  29865  cdj3lem2  30212  xdivval  30595  cvmlift3lem4  32569  scutval  33265  dmscut  33272  fvtransport  33493  finxpreclem4  34678  poimirlem26  34933  lshpkrlem1  36261  lshpkrlem2  36262  lshpkrlem3  36263  trlval  37313  cdleme31fv  37541  cdleme50f  37693  cdlemksv  37995  cdlemkuu  38046  cdlemk40  38068  cdlemk56  38122  cdlemm10N  38269  cdlemn11a  38358  dihval  38383  dihf11lem  38417  dihatlat  38485  dochfl1  38627  mapdhval  38875  hvmapvalvalN  38912  hdmap1vallem  38948  hdmapval  38979  hdmapfnN  38980  hgmapval  39038  hgmapfnN  39039  resubval  39217  mpaaval  39771  wessf1ornlem  41465