Theorem riotacl 7394

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃!wreu 3363  {crab 3412  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-un 4151  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  riotaeqimp  7403  riotaprop  7404  riotass2  7407  riotass  7408  riotaxfrd  7411  riotaclb  7418  supcl  9450  fisupcl  9462  ttrcltr  9717  htalem  9961  dfac8clem  10111  dfac2a  10208  fin23lem22  10405  zorn2lem1  10574  subcl  11556  divcl  11980  lbcl  12268  flcl  13935  cjf  15271  sqrtcl  15529  qnumdencl  16915  qnumdenbi  16920  catidcl  17856  lubcl  18529  glbcl  18542  ismgmid  18845  grpinvfval  19189  grpinvf  19197  pj1f  19911  nosupno  28060  nosupbday  28062  nosupbnd1  28071  noinfno  28075  noinfbday  28077  noinfbnd1  28086  cutcuts  28167  divsclw  28581  mirf  29132  midf  29281  ismidb  29283  lmif  29290  islmib  29292  uspgredg2vlem  29804  usgredg2vlem1  29806  frgrncvvdeqlem4  30903  grpoidcl  31116  grpoinvcl  31126  pjpreeq  32000  cnlnadjlem3  32671  adjbdln  32685  xdivcld  33489  cvmlift3lem3  36086  transportcl  36798  finxpreclem4  38318  poimirlem26  38565  iorlid  38793  riotaclbgBAD  40012  lshpkrlem2  40169  lshpkrcl  40174  cdleme25cl  41415  cdleme29cl  41435  cdlemefrs29clN  41457  cdlemk29-3  41969  cdlemkid5  41993  dihlsscpre  42292  mapdhcl  42785  hdmapcl  42888  hgmapcl  42947  primrootsunit1  43148  rernegcl  43423  rersubcl  43430  sn-subcl  43480  sn-redivcld  43496  fsuppind  43619  tfsconcatfv  44343  wessf1ornlem  46200  fourierdlem50  47166