Theorem riotacl 7332

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃!wreu 3348  {crab 3399  ℩crio 7314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448  df-riota 7315

This theorem is referenced by:  riotaeqimp  7341  riotaprop  7342  riotass2  7345  riotass  7346  riotaxfrd  7349  riotaclb  7356  supcl  9361  fisupcl  9373  ttrcltr  9625  htalem  9808  dfac8clem  9942  dfac2a  10040  fin23lem22  10237  zorn2lem1  10406  subcl  11379  divcl  11802  lbcl  12093  flcl  13715  cjf  15027  sqrtcl  15285  qnumdencl  16666  qnumdenbi  16671  catidcl  17605  lubcl  18278  glbcl  18291  ismgmid  18590  grpinvfval  18908  grpinvf  18916  pj1f  19626  nosupno  27671  nosupbday  27673  nosupbnd1  27682  noinfno  27686  noinfbday  27688  noinfbnd1  27697  cutcuts  27777  divsclw  28191  mirf  28732  midf  28848  ismidb  28850  lmif  28857  islmib  28859  uspgredg2vlem  29296  usgredg2vlem1  29298  frgrncvvdeqlem4  30377  grpoidcl  30589  grpoinvcl  30599  pjpreeq  31473  cnlnadjlem3  32144  adjbdln  32158  xdivcld  33004  cvmlift3lem3  35515  transportcl  36227  finxpreclem4  37599  poimirlem26  37847  iorlid  38059  riotaclbgBAD  39214  lshpkrlem2  39371  lshpkrcl  39376  cdleme25cl  40617  cdleme29cl  40637  cdlemefrs29clN  40659  cdlemk29-3  41171  cdlemkid5  41195  dihlsscpre  41494  mapdhcl  41987  hdmapcl  42090  hgmapcl  42149  primrootsunit1  42351  rernegcl  42626  rersubcl  42633  sn-subcl  42683  sn-redivcld  42699  fsuppind  42833  tfsconcatfv  43583  wessf1ornlem  45429  fourierdlem50  46400