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

Theorem riotaex 7110
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 7106 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
2 iotaex 6328 . 2 (℩𝑥(𝑥𝐴𝜓)) ∈ V
31, 2eqeltri 2907 1 (𝑥𝐴 𝜓) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 398  wcel 2108  Vcvv 3493  cio 6305  crio 7105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-nul 5201
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-sn 4560  df-pr 4562  df-uni 4831  df-iota 6307  df-riota 7106
This theorem is referenced by:  ordtypelem3  8976  dfac8clem  9450  zorn2lem1  9910  subval  10869  1div0  11291  divval  11292  elq  12342  flval  13156  ceilval2  13202  cjval  14453  sqrtval  14588  sqrtf  14715  cidval  16940  cidfn  16942  lubdm  17581  lubval  17586  glbdm  17594  glbval  17599  grpinvfval  18134  grpinvval  18136  grpinvfn  18137  pj1val  18813  evlsval  20291  q1pval  24739  ig1pval  24758  coeval  24805  quotval  24873  mirfv  26434  mirf  26438  usgredg2v  27001  frgrncvvdeqlem5  28074  1div0apr  28239  gidval  28281  grpoinvval  28292  grpoinvf  28301  pjhval  29166  pjfni  29470  cnlnadjlem5  29840  nmopadjlei  29857  cdj3lem2  30204  xdivval  30588  cvmlift3lem4  32562  scutval  33258  dmscut  33265  fvtransport  33486  finxpreclem4  34667  poimirlem26  34910  lshpkrlem1  36238  lshpkrlem2  36239  lshpkrlem3  36240  trlval  37290  cdleme31fv  37518  cdleme50f  37670  cdlemksv  37972  cdlemkuu  38023  cdlemk40  38045  cdlemk56  38099  cdlemm10N  38246  cdlemn11a  38335  dihval  38360  dihf11lem  38394  dihatlat  38462  dochfl1  38604  mapdhval  38852  hvmapvalvalN  38889  hdmap1vallem  38925  hdmapval  38956  hdmapfnN  38957  hgmapval  39015  hgmapfnN  39016  resubval  39187  mpaaval  39741  wessf1ornlem  41434
  Copyright terms: Public domain W3C validator