Theorem riotacl 7230

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃!wreu 3065  {crab 3067  ℩crio 7211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376  df-riota 7212

This theorem is referenced by:  riotaeqimp  7239  riotaprop  7240  riotass2  7243  riotass  7244  riotaxfrd  7247  riotaclb  7254  supcl  9147  fisupcl  9158  htalem  9585  dfac8clem  9719  dfac2a  9816  fin23lem22  10014  zorn2lem1  10183  subcl  11150  divcl  11569  lbcl  11856  flcl  13443  cjf  14743  sqrtcl  15001  qnumdencl  16371  qnumdenbi  16376  catidcl  17308  lubcl  17990  glbcl  18003  ismgmid  18264  grpinvfval  18533  grpinvf  18541  pj1f  19218  mirf  26925  midf  27041  ismidb  27043  lmif  27050  islmib  27052  uspgredg2vlem  27493  usgredg2vlem1  27495  frgrncvvdeqlem4  28567  grpoidcl  28777  grpoinvcl  28787  pjpreeq  29661  cnlnadjlem3  30332  adjbdln  30346  xdivcld  31099  cvmlift3lem3  33183  ttrcltr  33702  nosupno  33833  nosupbday  33835  nosupbnd1  33844  noinfno  33848  noinfbday  33850  noinfbnd1  33859  scutcut  33922  transportcl  34262  finxpreclem4  35492  poimirlem26  35730  iorlid  35943  riotaclbgBAD  36895  lshpkrlem2  37052  lshpkrcl  37057  cdleme25cl  38298  cdleme29cl  38318  cdlemefrs29clN  38340  cdlemk29-3  38852  cdlemkid5  38876  dihlsscpre  39175  mapdhcl  39668  hdmapcl  39771  hgmapcl  39830  fsuppind  40202  rernegcl  40275  rersubcl  40282  sn-subcl  40330  wessf1ornlem  42611  fourierdlem50  43587