Theorem riotacl 7405

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃!wreu 3376  {crab 3433  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-un 3968  df-ss 3980  df-sn 4632  df-pr 4634  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  riotaeqimp  7414  riotaprop  7415  riotass2  7418  riotass  7419  riotaxfrd  7422  riotaclb  7429  supcl  9496  fisupcl  9507  ttrcltr  9754  htalem  9934  dfac8clem  10070  dfac2a  10168  fin23lem22  10365  zorn2lem1  10534  subcl  11505  divcl  11926  lbcl  12217  flcl  13832  cjf  15140  sqrtcl  15397  qnumdencl  16773  qnumdenbi  16778  catidcl  17727  lubcl  18415  glbcl  18428  ismgmid  18691  grpinvfval  19009  grpinvf  19017  pj1f  19730  nosupno  27763  nosupbday  27765  nosupbnd1  27774  noinfno  27778  noinfbday  27780  noinfbnd1  27789  scutcut  27861  divsclw  28235  mirf  28683  midf  28799  ismidb  28801  lmif  28808  islmib  28810  uspgredg2vlem  29255  usgredg2vlem1  29257  frgrncvvdeqlem4  30331  grpoidcl  30543  grpoinvcl  30553  pjpreeq  31427  cnlnadjlem3  32098  adjbdln  32112  xdivcld  32890  cvmlift3lem3  35306  transportcl  36015  finxpreclem4  37377  poimirlem26  37633  iorlid  37845  riotaclbgBAD  38936  lshpkrlem2  39093  lshpkrcl  39098  cdleme25cl  40340  cdleme29cl  40360  cdlemefrs29clN  40382  cdlemk29-3  40894  cdlemkid5  40918  dihlsscpre  41217  mapdhcl  41710  hdmapcl  41813  hgmapcl  41872  primrootsunit1  42079  rernegcl  42378  rersubcl  42385  sn-subcl  42434  fsuppind  42577  tfsconcatfv  43331  wessf1ornlem  45128  fourierdlem50  46112