Theorem riotacl 6525

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 3650	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 6524	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sseldi 3566	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1977  ∃!wreu 2898  {crab 2900  ℩crio 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-riota 6511

This theorem is referenced by:  riotaprop  6534  riotass2  6537  riotass  6538  riotaxfrd  6541  riotaclb  6548  supcl  8247  fisupcl  8258  htalem  8642  dfac8clem  8738  dfac2a  8835  fin23lem22  9032  zorn2lem1  9201  subcl  10159  divcl  10570  lbcl  10853  flcl  12458  cjf  13692  sqrtcl  13949  qnumdencl  15285  qnumdenbi  15290  catidcl  16166  lubcl  16808  glbcl  16821  ismgmid  17087  grpinvf  17289  pj1f  17933  mirf  25355  midf  25468  ismidb  25470  lmif  25477  islmib  25479  usgraidx2vlem1  25920  nbgraf1olem2  25971  frgrancvvdeqlem5  26561  grpoidcl  26752  grpoinvcl  26762  pjpreeq  27641  cnlnadjlem3  28312  adjbdln  28326  xdivcld  28962  cvmlift3lem3  30557  transportcl  31310  finxpreclem4  32407  poimirlem26  32605  iorlid  32827  riotaclbgBAD  33258  lshpkrlem2  33416  lshpkrcl  33421  cdleme25cl  34663  cdleme29cl  34683  cdlemefrs29clN  34705  cdlemk29-3  35217  cdlemkid5  35241  dihlsscpre  35541  mapdhcl  36034  hdmapcl  36140  hgmapcl  36199  wessf1ornlem  38366  fourierdlem50  39049  riotaeqimp  40338  uspgredg2vlem  40450  usgredg2vlem1  40452  frgrncvvdeqlem5  41473