Theorem riotacl 7384

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃!wreu 3362  {crab 3420  ℩crio 7366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-un 3936  df-ss 3948  df-sn 4607  df-pr 4609  df-uni 4889  df-iota 6489  df-riota 7367

This theorem is referenced by:  riotaeqimp  7393  riotaprop  7394  riotass2  7397  riotass  7398  riotaxfrd  7401  riotaclb  7408  supcl  9475  fisupcl  9487  ttrcltr  9735  htalem  9915  dfac8clem  10051  dfac2a  10149  fin23lem22  10346  zorn2lem1  10515  subcl  11486  divcl  11907  lbcl  12198  flcl  13817  cjf  15128  sqrtcl  15385  qnumdencl  16763  qnumdenbi  16768  catidcl  17699  lubcl  18372  glbcl  18385  ismgmid  18648  grpinvfval  18966  grpinvf  18974  pj1f  19683  nosupno  27672  nosupbday  27674  nosupbnd1  27683  noinfno  27687  noinfbday  27689  noinfbnd1  27698  scutcut  27770  divsclw  28155  mirf  28644  midf  28760  ismidb  28762  lmif  28769  islmib  28771  uspgredg2vlem  29207  usgredg2vlem1  29209  frgrncvvdeqlem4  30288  grpoidcl  30500  grpoinvcl  30510  pjpreeq  31384  cnlnadjlem3  32055  adjbdln  32069  xdivcld  32902  cvmlift3lem3  35348  transportcl  36056  finxpreclem4  37417  poimirlem26  37675  iorlid  37887  riotaclbgBAD  38977  lshpkrlem2  39134  lshpkrcl  39139  cdleme25cl  40381  cdleme29cl  40401  cdlemefrs29clN  40423  cdlemk29-3  40935  cdlemkid5  40959  dihlsscpre  41258  mapdhcl  41751  hdmapcl  41854  hgmapcl  41913  primrootsunit1  42115  rernegcl  42389  rersubcl  42396  sn-subcl  42445  fsuppind  42588  tfsconcatfv  43340  wessf1ornlem  45189  fourierdlem50  46165