Theorem riotacl 7384

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃!wreu 3367  {crab 3416  ℩crio 7366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-un 3910  df-ss 3922  df-sn 4590  df-pr 4592  df-uni 4873  df-iota 6492  df-riota 7367

This theorem is referenced by:  riotaeqimp  7393  riotaprop  7394  riotass2  7397  riotass  7398  riotaxfrd  7401  riotaclb  7408  supcl  9414  fisupcl  9426  ttrcltr  9681  htalem  9878  dfac8clem  10012  dfac2a  10109  fin23lem22  10306  zorn2lem1  10475  subcl  11451  divcl  11873  lbcl  12161  flcl  13824  cjf  15151  sqrtcl  15409  qnumdencl  16793  qnumdenbi  16798  catidcl  17733  lubcl  18406  glbcl  18419  ismgmid  18718  grpinvfval  19040  grpinvf  19048  pj1f  19762  nosupno  27867  nosupbday  27869  nosupbnd1  27878  noinfno  27882  noinfbday  27884  noinfbnd1  27893  cutcuts  27974  divsclw  28388  mirf  28937  midf  29085  ismidb  29087  lmif  29094  islmib  29096  uspgredg2vlem  29573  usgredg2vlem1  29575  frgrncvvdeqlem4  30653  grpoidcl  30866  grpoinvcl  30876  pjpreeq  31750  cnlnadjlem3  32421  adjbdln  32435  xdivcld  33242  cvmlift3lem3  35813  transportcl  36525  finxpreclem4  38040  poimirlem26  38297  iorlid  38509  riotaclbgBAD  39728  lshpkrlem2  39885  lshpkrcl  39890  cdleme25cl  41131  cdleme29cl  41151  cdlemefrs29clN  41173  cdlemk29-3  41685  cdlemkid5  41709  dihlsscpre  42008  mapdhcl  42501  hdmapcl  42604  hgmapcl  42663  primrootsunit1  42864  rernegcl  43132  rersubcl  43139  sn-subcl  43189  sn-redivcld  43205  fsuppind  43322  tfsconcatfv  44068  wessf1ornlem  45903  fourierdlem50  46870