Theorem riotacl 7406

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃!wreu 3377  {crab 3435  ℩crio 7388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-un 3955  df-ss 3967  df-sn 4626  df-pr 4628  df-uni 4907  df-iota 6513  df-riota 7389

This theorem is referenced by:  riotaeqimp  7415  riotaprop  7416  riotass2  7419  riotass  7420  riotaxfrd  7423  riotaclb  7430  supcl  9499  fisupcl  9510  ttrcltr  9757  htalem  9937  dfac8clem  10073  dfac2a  10171  fin23lem22  10368  zorn2lem1  10537  subcl  11508  divcl  11929  lbcl  12220  flcl  13836  cjf  15144  sqrtcl  15401  qnumdencl  16777  qnumdenbi  16782  catidcl  17726  lubcl  18403  glbcl  18416  ismgmid  18679  grpinvfval  18997  grpinvf  19005  pj1f  19716  nosupno  27749  nosupbday  27751  nosupbnd1  27760  noinfno  27764  noinfbday  27766  noinfbnd1  27775  scutcut  27847  divsclw  28221  mirf  28669  midf  28785  ismidb  28787  lmif  28794  islmib  28796  uspgredg2vlem  29241  usgredg2vlem1  29243  frgrncvvdeqlem4  30322  grpoidcl  30534  grpoinvcl  30544  pjpreeq  31418  cnlnadjlem3  32089  adjbdln  32103  xdivcld  32906  cvmlift3lem3  35327  transportcl  36035  finxpreclem4  37396  poimirlem26  37654  iorlid  37866  riotaclbgBAD  38956  lshpkrlem2  39113  lshpkrcl  39118  cdleme25cl  40360  cdleme29cl  40380  cdlemefrs29clN  40402  cdlemk29-3  40914  cdlemkid5  40938  dihlsscpre  41237  mapdhcl  41730  hdmapcl  41833  hgmapcl  41892  primrootsunit1  42099  rernegcl  42406  rersubcl  42413  sn-subcl  42462  fsuppind  42605  tfsconcatfv  43359  wessf1ornlem  45195  fourierdlem50  46176