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

Theorem riotacl 7126
Description: Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
Assertion
Ref Expression
riotacl (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem riotacl
StepHypRef Expression
1 ssrab2 4059 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
2 riotacl2 7125 . 2 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ {𝑥𝐴𝜑})
31, 2sseldi 3968 1 (∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  ∃!wreu 3144  {crab 3146  crio 7108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-un 3944  df-in 3946  df-ss 3955  df-sn 4564  df-pr 4566  df-uni 4837  df-iota 6311  df-riota 7109
This theorem is referenced by:  riotaeqimp  7135  riotaprop  7136  riotass2  7139  riotass  7140  riotaxfrd  7143  riotaclb  7150  supcl  8914  fisupcl  8925  htalem  9317  dfac8clem  9450  dfac2a  9547  fin23lem22  9741  zorn2lem1  9910  subcl  10877  divcl  11296  lbcl  11584  flcl  13158  cjf  14456  sqrtcl  14714  qnumdencl  16071  qnumdenbi  16076  catidcl  16945  lubcl  17587  glbcl  17600  ismgmid  17866  grpinvfval  18074  grpinvf  18082  pj1f  18745  mirf  26360  midf  26476  ismidb  26478  lmif  26485  islmib  26487  uspgredg2vlem  26919  usgredg2vlem1  26921  frgrncvvdeqlem4  27995  grpoidcl  28205  grpoinvcl  28215  pjpreeq  29089  cnlnadjlem3  29760  adjbdln  29774  xdivcld  30513  cvmlift3lem3  32452  nosupno  33087  nosupbday  33089  nosupbnd1  33098  scutcut  33150  transportcl  33378  finxpreclem4  34544  poimirlem26  34785  iorlid  35004  riotaclbgBAD  35957  lshpkrlem2  36114  lshpkrcl  36119  cdleme25cl  37360  cdleme29cl  37380  cdlemefrs29clN  37402  cdlemk29-3  37914  cdlemkid5  37938  dihlsscpre  38237  mapdhcl  38730  hdmapcl  38833  hgmapcl  38892  rernegcl  39064  rersubcl  39071  wessf1ornlem  41306  fourierdlem50  42303
  Copyright terms: Public domain W3C validator