Theorem riotacl 7385

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 4042	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 7384	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sselid 3943	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2149  ∃!wreu 3374  {crab 3423  ℩crio 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-un 3918  df-ss 3930  df-sn 4595  df-pr 4597  df-uni 4877  df-iota 6493  df-riota 7368

This theorem is referenced by:  riotaeqimp  7394  riotaprop  7395  riotass2  7398  riotass  7399  riotaxfrd  7402  riotaclb  7409  supcl  9417  fisupcl  9429  ttrcltr  9684  htalem  9881  dfac8clem  10015  dfac2a  10112  fin23lem22  10310  zorn2lem1  10479  subcl  11455  divcl  11877  lbcl  12165  flcl  13827  cjf  15154  sqrtcl  15412  qnumdencl  16797  qnumdenbi  16802  catidcl  17737  lubcl  18410  glbcl  18423  ismgmid  18722  grpinvfval  19044  grpinvf  19052  pj1f  19766  nosupno  27832  nosupbday  27834  nosupbnd1  27843  noinfno  27847  noinfbday  27849  noinfbnd1  27858  cutcuts  27939  divsclw  28353  mirf  28898  midf  29042  ismidb  29044  lmif  29051  islmib  29053  uspgredg2vlem  29513  usgredg2vlem1  29515  frgrncvvdeqlem4  30593  grpoidcl  30806  grpoinvcl  30816  pjpreeq  31690  cnlnadjlem3  32361  adjbdln  32375  xdivcld  33182  cvmlift3lem3  35711  transportcl  36423  finxpreclem4  37927  poimirlem26  38184  iorlid  38396  riotaclbgBAD  39617  lshpkrlem2  39774  lshpkrcl  39779  cdleme25cl  41020  cdleme29cl  41040  cdlemefrs29clN  41062  cdlemk29-3  41574  cdlemkid5  41598  dihlsscpre  41897  mapdhcl  42390  hdmapcl  42493  hgmapcl  42552  primrootsunit1  42753  rernegcl  43021  rersubcl  43028  sn-subcl  43078  sn-redivcld  43094  fsuppind  43213  tfsconcatfv  43959  wessf1ornlem  45794  fourierdlem50  46761