Theorem riotacl 7110

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 4007	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 7109	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sseldi 3913	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111  ∃!wreu 3108  {crab 3110  ℩crio 7092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-uni 4801  df-iota 6283  df-riota 7093

This theorem is referenced by:  riotaeqimp  7119  riotaprop  7120  riotass2  7123  riotass  7124  riotaxfrd  7127  riotaclb  7134  supcl  8906  fisupcl  8917  htalem  9309  dfac8clem  9443  dfac2a  9540  fin23lem22  9738  zorn2lem1  9907  subcl  10874  divcl  11293  lbcl  11579  flcl  13160  cjf  14455  sqrtcl  14713  qnumdencl  16069  qnumdenbi  16074  catidcl  16945  lubcl  17587  glbcl  17600  ismgmid  17867  grpinvfval  18134  grpinvf  18142  pj1f  18815  mirf  26454  midf  26570  ismidb  26572  lmif  26579  islmib  26581  uspgredg2vlem  27013  usgredg2vlem1  27015  frgrncvvdeqlem4  28087  grpoidcl  28297  grpoinvcl  28307  pjpreeq  29181  cnlnadjlem3  29852  adjbdln  29866  xdivcld  30625  cvmlift3lem3  32681  nosupno  33316  nosupbday  33318  nosupbnd1  33327  scutcut  33379  transportcl  33607  finxpreclem4  34811  poimirlem26  35083  iorlid  35296  riotaclbgBAD  36250  lshpkrlem2  36407  lshpkrcl  36412  cdleme25cl  37653  cdleme29cl  37673  cdlemefrs29clN  37695  cdlemk29-3  38207  cdlemkid5  38231  dihlsscpre  38530  mapdhcl  39023  hdmapcl  39126  hgmapcl  39185  fsuppind  39456  rernegcl  39509  rersubcl  39516  sn-subcl  39564  wessf1ornlem  41811  fourierdlem50  42798