Theorem riotacl 7385

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃!wreu 3374  {crab 3432  ℩crio 7366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6495  df-riota 7367

This theorem is referenced by:  riotaeqimp  7394  riotaprop  7395  riotass2  7398  riotass  7399  riotaxfrd  7402  riotaclb  7409  supcl  9455  fisupcl  9466  ttrcltr  9713  htalem  9893  dfac8clem  10029  dfac2a  10126  fin23lem22  10324  zorn2lem1  10493  subcl  11461  divcl  11880  lbcl  12167  flcl  13762  cjf  15053  sqrtcl  15310  qnumdencl  16677  qnumdenbi  16682  catidcl  17628  lubcl  18312  glbcl  18325  ismgmid  18586  grpinvfval  18865  grpinvf  18873  pj1f  19567  nosupno  27213  nosupbday  27215  nosupbnd1  27224  noinfno  27228  noinfbday  27230  noinfbnd1  27239  scutcut  27310  divsclw  27652  mirf  27949  midf  28065  ismidb  28067  lmif  28074  islmib  28076  uspgredg2vlem  28518  usgredg2vlem1  28520  frgrncvvdeqlem4  29593  grpoidcl  29805  grpoinvcl  29815  pjpreeq  30689  cnlnadjlem3  31360  adjbdln  31374  xdivcld  32127  cvmlift3lem3  34381  transportcl  35074  finxpreclem4  36361  poimirlem26  36600  iorlid  36812  riotaclbgBAD  37910  lshpkrlem2  38067  lshpkrcl  38072  cdleme25cl  39314  cdleme29cl  39334  cdlemefrs29clN  39356  cdlemk29-3  39868  cdlemkid5  39892  dihlsscpre  40191  mapdhcl  40684  hdmapcl  40787  hgmapcl  40846  fsuppind  41244  rernegcl  41326  rersubcl  41333  sn-subcl  41382  tfsconcatfv  42173  wessf1ornlem  43963  fourierdlem50  44951