Theorem riotacl 7393

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃!wreu 3369  {crab 3418  ℩crio 7375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594  df-uni 4875  df-iota 6496  df-riota 7376

This theorem is used by:  riotaeqimp  7402  riotaprop  7403  riotass2  7406  riotass  7407  riotaxfrd  7410  riotaclb  7417  supcl  9425  fisupcl  9437  ttrcltr  9692  htalem  9897  dfac8clem  10032  dfac2a  10129  fin23lem22  10326  zorn2lem1  10495  subcl  11471  divcl  11893  lbcl  12181  flcl  13846  cjf  15179  sqrtcl  15437  qnumdencl  16820  qnumdenbi  16825  catidcl  17760  lubcl  18433  glbcl  18446  ismgmid  18748  grpinvfval  19089  grpinvf  19097  pj1f  19811  nosupno  27918  nosupbday  27920  nosupbnd1  27929  noinfno  27933  noinfbday  27935  noinfbnd1  27944  cutcuts  28025  divsclw  28439  mirf  28988  midf  29136  ismidb  29138  lmif  29145  islmib  29147  uspgredg2vlem  29631  usgredg2vlem1  29633  frgrncvvdeqlem4  30724  grpoidcl  30937  grpoinvcl  30947  pjpreeq  31821  cnlnadjlem3  32492  adjbdln  32506  xdivcld  33312  cvmlift3lem3  35850  transportcl  36562  finxpreclem4  38097  poimirlem26  38354  iorlid  38567  riotaclbgBAD  39786  lshpkrlem2  39943  lshpkrcl  39948  cdleme25cl  41189  cdleme29cl  41209  cdlemefrs29clN  41231  cdlemk29-3  41743  cdlemkid5  41767  dihlsscpre  42066  mapdhcl  42559  hdmapcl  42662  hgmapcl  42721  primrootsunit1  42922  rernegcl  43190  rersubcl  43197  sn-subcl  43247  sn-redivcld  43263  fsuppind  43380  tfsconcatfv  44126  wessf1ornlem  45961  fourierdlem50  46928