Theorem riotacl 7336

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃!wreu 3349  {crab 3405  ℩crio 7317

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-un 3918  df-in 3920  df-ss 3930  df-sn 4592  df-pr 4594  df-uni 4871  df-iota 6453  df-riota 7318

This theorem is referenced by:  riotaeqimp  7345  riotaprop  7346  riotass2  7349  riotass  7350  riotaxfrd  7353  riotaclb  7360  supcl  9403  fisupcl  9414  ttrcltr  9661  htalem  9841  dfac8clem  9977  dfac2a  10074  fin23lem22  10272  zorn2lem1  10441  subcl  11409  divcl  11828  lbcl  12115  flcl  13710  cjf  15001  sqrtcl  15258  qnumdencl  16625  qnumdenbi  16630  catidcl  17576  lubcl  18260  glbcl  18273  ismgmid  18534  grpinvfval  18803  grpinvf  18811  pj1f  19493  nosupno  27088  nosupbday  27090  nosupbnd1  27099  noinfno  27103  noinfbday  27105  noinfbnd1  27114  scutcut  27183  mirf  27665  midf  27781  ismidb  27783  lmif  27790  islmib  27792  uspgredg2vlem  28234  usgredg2vlem1  28236  frgrncvvdeqlem4  29309  grpoidcl  29519  grpoinvcl  29529  pjpreeq  30403  cnlnadjlem3  31074  adjbdln  31088  xdivcld  31849  cvmlift3lem3  34002  transportcl  34694  finxpreclem4  35938  poimirlem26  36177  iorlid  36390  riotaclbgBAD  37489  lshpkrlem2  37646  lshpkrcl  37651  cdleme25cl  38893  cdleme29cl  38913  cdlemefrs29clN  38935  cdlemk29-3  39447  cdlemkid5  39471  dihlsscpre  39770  mapdhcl  40263  hdmapcl  40366  hgmapcl  40425  fsuppind  40823  rernegcl  40898  rersubcl  40905  sn-subcl  40954  tfsconcatfv  41734  wessf1ornlem  43525  fourierdlem50  44517