Theorem riotacl 7330

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃!wreu 3346  {crab 3397  ℩crio 7312

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 2182  ax-ext 2706

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-un 3904  df-ss 3916  df-sn 4579  df-pr 4581  df-uni 4862  df-iota 6446  df-riota 7313

This theorem is referenced by:  riotaeqimp  7339  riotaprop  7340  riotass2  7343  riotass  7344  riotaxfrd  7347  riotaclb  7354  supcl  9359  fisupcl  9371  ttrcltr  9623  htalem  9806  dfac8clem  9940  dfac2a  10038  fin23lem22  10235  zorn2lem1  10404  subcl  11377  divcl  11800  lbcl  12091  flcl  13713  cjf  15025  sqrtcl  15283  qnumdencl  16664  qnumdenbi  16669  catidcl  17603  lubcl  18276  glbcl  18289  ismgmid  18588  grpinvfval  18906  grpinvf  18914  pj1f  19624  nosupno  27669  nosupbday  27671  nosupbnd1  27680  noinfno  27684  noinfbday  27686  noinfbnd1  27695  scutcut  27769  divsclw  28164  mirf  28681  midf  28797  ismidb  28799  lmif  28806  islmib  28808  uspgredg2vlem  29245  usgredg2vlem1  29247  frgrncvvdeqlem4  30326  grpoidcl  30538  grpoinvcl  30548  pjpreeq  31422  cnlnadjlem3  32093  adjbdln  32107  xdivcld  32953  cvmlift3lem3  35464  transportcl  36176  finxpreclem4  37538  poimirlem26  37786  iorlid  37998  riotaclbgBAD  39153  lshpkrlem2  39310  lshpkrcl  39315  cdleme25cl  40556  cdleme29cl  40576  cdlemefrs29clN  40598  cdlemk29-3  41110  cdlemkid5  41134  dihlsscpre  41433  mapdhcl  41926  hdmapcl  42029  hgmapcl  42088  primrootsunit1  42290  rernegcl  42568  rersubcl  42575  sn-subcl  42625  sn-redivcld  42641  fsuppind  42775  tfsconcatfv  43525  wessf1ornlem  45371  fourierdlem50  46342