Theorem riotacl 7383

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃!wreu 3375  {crab 3433  ℩crio 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-riota 7365

This theorem is referenced by:  riotaeqimp  7392  riotaprop  7393  riotass2  7396  riotass  7397  riotaxfrd  7400  riotaclb  7407  supcl  9453  fisupcl  9464  ttrcltr  9711  htalem  9891  dfac8clem  10027  dfac2a  10124  fin23lem22  10322  zorn2lem1  10491  subcl  11459  divcl  11878  lbcl  12165  flcl  13760  cjf  15051  sqrtcl  15308  qnumdencl  16675  qnumdenbi  16680  catidcl  17626  lubcl  18310  glbcl  18323  ismgmid  18584  grpinvfval  18863  grpinvf  18871  pj1f  19565  nosupno  27206  nosupbday  27208  nosupbnd1  27217  noinfno  27221  noinfbday  27223  noinfbnd1  27232  scutcut  27302  divsclw  27642  mirf  27911  midf  28027  ismidb  28029  lmif  28036  islmib  28038  uspgredg2vlem  28480  usgredg2vlem1  28482  frgrncvvdeqlem4  29555  grpoidcl  29767  grpoinvcl  29777  pjpreeq  30651  cnlnadjlem3  31322  adjbdln  31336  xdivcld  32089  cvmlift3lem3  34312  transportcl  35005  finxpreclem4  36275  poimirlem26  36514  iorlid  36726  riotaclbgBAD  37824  lshpkrlem2  37981  lshpkrcl  37986  cdleme25cl  39228  cdleme29cl  39248  cdlemefrs29clN  39270  cdlemk29-3  39782  cdlemkid5  39806  dihlsscpre  40105  mapdhcl  40598  hdmapcl  40701  hgmapcl  40760  fsuppind  41162  rernegcl  41244  rersubcl  41251  sn-subcl  41300  tfsconcatfv  42091  wessf1ornlem  43882  fourierdlem50  44872