Theorem riotacl 7398

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃!wreu 3363  {crab 3412  ℩crio 7380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-un 4150  df-sn 4585  df-pr 4587  df-uni 4867  df-iota 6497  df-riota 7381

This theorem is used by:  riotaeqimp  7407  riotaprop  7408  riotass2  7411  riotass  7412  riotaxfrd  7415  riotaclb  7422  supcl  9457  fisupcl  9469  ttrcltr  9724  htalem  9968  dfac8clem  10118  dfac2a  10215  fin23lem22  10412  zorn2lem1  10581  subcl  11563  divcl  11987  lbcl  12275  flcl  13942  cjf  15280  sqrtcl  15538  qnumdencl  16924  qnumdenbi  16929  catidcl  17865  lubcl  18538  glbcl  18551  ismgmid  18854  grpinvfval  19198  grpinvf  19206  pj1f  19920  nosupno  28069  nosupbday  28071  nosupbnd1  28080  noinfno  28084  noinfbday  28086  noinfbnd1  28095  cutcuts  28176  divsclw  28590  mirf  29141  midf  29290  ismidb  29292  lmif  29299  islmib  29301  uspgredg2vlem  29813  usgredg2vlem1  29815  frgrncvvdeqlem4  30912  grpoidcl  31125  grpoinvcl  31135  pjpreeq  32009  cnlnadjlem3  32680  adjbdln  32694  xdivcld  33539  cvmlift3lem3  36204  transportcl  36922  finxpreclem4  38454  poimirlem26  38701  iorlid  38929  riotaclbgBAD  40148  lshpkrlem2  40305  lshpkrcl  40310  cdleme25cl  41551  cdleme29cl  41571  cdlemefrs29clN  41593  cdlemk29-3  42105  cdlemkid5  42129  dihlsscpre  42428  mapdhcl  42921  hdmapcl  43024  hgmapcl  43083  primrootsunit1  43284  rernegcl  43559  rersubcl  43566  sn-subcl  43616  sn-redivcld  43632  fsuppind  43755  tfsconcatfv  44480  wessf1ornlem  46336  fourierdlem50  47302