Theorem riotacl 7370

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

Step	Hyp	Ref	Expression
1		ssrab2 4033	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 7369	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sselid 3934	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2142  ∃!wreu 3365  {crab 3414  ℩crio 7352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-un 3909  df-ss 3921  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6477  df-riota 7353

This theorem is referenced by:  riotaeqimp  7379  riotaprop  7380  riotass2  7383  riotass  7384  riotaxfrd  7387  riotaclb  7394  supcl  9404  fisupcl  9416  ttrcltr  9671  htalem  9854  dfac8clem  9988  dfac2a  10086  fin23lem22  10284  zorn2lem1  10453  subcl  11429  divcl  11851  lbcl  12143  flcl  13805  cjf  15131  sqrtcl  15389  qnumdencl  16774  qnumdenbi  16779  catidcl  17714  lubcl  18387  glbcl  18400  ismgmid  18699  grpinvfval  19020  grpinvf  19028  pj1f  19737  nosupno  27767  nosupbday  27769  nosupbnd1  27778  noinfno  27782  noinfbday  27784  noinfbnd1  27793  cutcuts  27874  divsclw  28288  mirf  28833  midf  28949  ismidb  28951  lmif  28958  islmib  28960  uspgredg2vlem  29424  usgredg2vlem1  29426  frgrncvvdeqlem4  30504  grpoidcl  30717  grpoinvcl  30727  pjpreeq  31601  cnlnadjlem3  32272  adjbdln  32286  xdivcld  33100  cvmlift3lem3  35671  transportcl  36383  finxpreclem4  37888  poimirlem26  38145  iorlid  38357  riotaclbgBAD  39578  lshpkrlem2  39735  lshpkrcl  39740  cdleme25cl  40981  cdleme29cl  41001  cdlemefrs29clN  41023  cdlemk29-3  41535  cdlemkid5  41559  dihlsscpre  41858  mapdhcl  42351  hdmapcl  42454  hgmapcl  42513  primrootsunit1  42714  rernegcl  42980  rersubcl  42987  sn-subcl  43037  sn-redivcld  43053  fsuppind  43172  tfsconcatfv  43918  wessf1ornlem  45763  fourierdlem50  46730