MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riotaex Structured version   Visualization version   GIF version

Theorem riotaex 7107
Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
riotaex (𝑥𝐴 𝜓) ∈ V

Proof of Theorem riotaex
StepHypRef Expression
1 df-riota 7103 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
2 iotaex 6328 . 2 (℩𝑥(𝑥𝐴𝜓)) ∈ V
31, 2eqeltri 2906 1 (𝑥𝐴 𝜓) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  Vcvv 3492  cio 6305  crio 7102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-sn 4558  df-pr 4560  df-uni 4831  df-iota 6307  df-riota 7103
This theorem is referenced by:  ordtypelem3  8972  dfac8clem  9446  zorn2lem1  9906  subval  10865  1div0  11287  divval  11288  elq  12338  flval  13152  ceilval2  13198  cjval  14449  sqrtval  14584  sqrtf  14711  cidval  16936  cidfn  16938  lubdm  17577  lubval  17582  glbdm  17590  glbval  17595  grpinvfval  18080  grpinvval  18082  grpinvfn  18083  pj1val  18750  evlsval  20227  q1pval  24674  ig1pval  24693  coeval  24740  quotval  24808  mirfv  26369  mirf  26373  usgredg2v  26936  frgrncvvdeqlem5  28009  1div0apr  28174  gidval  28216  grpoinvval  28227  grpoinvf  28236  pjhval  29101  pjfni  29405  cnlnadjlem5  29775  nmopadjlei  29792  cdj3lem2  30139  xdivval  30522  cvmlift3lem4  32466  scutval  33162  dmscut  33169  fvtransport  33390  finxpreclem4  34557  poimirlem26  34799  lshpkrlem1  36126  lshpkrlem2  36127  lshpkrlem3  36128  trlval  37178  cdleme31fv  37406  cdleme50f  37558  cdlemksv  37860  cdlemkuu  37911  cdlemk40  37933  cdlemk56  37987  cdlemm10N  38134  cdlemn11a  38223  dihval  38248  dihf11lem  38282  dihatlat  38350  dochfl1  38492  mapdhval  38740  hvmapvalvalN  38777  hdmap1vallem  38813  hdmapval  38844  hdmapfnN  38845  hgmapval  38903  hgmapfnN  38904  resubval  39075  mpaaval  39629  wessf1ornlem  41321
  Copyright terms: Public domain W3C validator