Theorem riotacl 7342

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃!wreu 3350  {crab 3401  ℩crio 7324

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6456  df-riota 7325

This theorem is referenced by:  riotaeqimp  7351  riotaprop  7352  riotass2  7355  riotass  7356  riotaxfrd  7359  riotaclb  7366  supcl  9373  fisupcl  9385  ttrcltr  9637  htalem  9820  dfac8clem  9954  dfac2a  10052  fin23lem22  10249  zorn2lem1  10418  subcl  11391  divcl  11814  lbcl  12105  flcl  13727  cjf  15039  sqrtcl  15297  qnumdencl  16678  qnumdenbi  16683  catidcl  17617  lubcl  18290  glbcl  18303  ismgmid  18602  grpinvfval  18920  grpinvf  18928  pj1f  19638  nosupno  27683  nosupbday  27685  nosupbnd1  27694  noinfno  27698  noinfbday  27700  noinfbnd1  27709  cutcuts  27789  divsclw  28203  mirf  28744  midf  28860  ismidb  28862  lmif  28869  islmib  28871  uspgredg2vlem  29308  usgredg2vlem1  29310  frgrncvvdeqlem4  30389  grpoidcl  30602  grpoinvcl  30612  pjpreeq  31486  cnlnadjlem3  32157  adjbdln  32171  xdivcld  33015  cvmlift3lem3  35537  transportcl  36249  finxpreclem4  37649  poimirlem26  37897  iorlid  38109  riotaclbgBAD  39330  lshpkrlem2  39487  lshpkrcl  39492  cdleme25cl  40733  cdleme29cl  40753  cdlemefrs29clN  40775  cdlemk29-3  41287  cdlemkid5  41311  dihlsscpre  41610  mapdhcl  42103  hdmapcl  42206  hgmapcl  42265  primrootsunit1  42467  rernegcl  42741  rersubcl  42748  sn-subcl  42798  sn-redivcld  42814  fsuppind  42948  tfsconcatfv  43698  wessf1ornlem  45544  fourierdlem50  46514