Theorem riotacl 6897

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃!wreu 3092  {crab 3094  ℩crio 6882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-un 3797  df-in 3799  df-ss 3806  df-sn 4399  df-pr 4401  df-uni 4672  df-iota 6099  df-riota 6883

This theorem is referenced by:  riotaeqimp  6906  riotaprop  6907  riotass2  6910  riotass  6911  riotaxfrd  6914  riotaclb  6921  supcl  8652  fisupcl  8663  htalem  9056  dfac8clem  9188  dfac2a  9285  fin23lem22  9484  zorn2lem1  9653  subcl  10621  divcl  11039  lbcl  11328  flcl  12915  cjf  14251  sqrtcl  14508  qnumdencl  15851  qnumdenbi  15856  catidcl  16728  lubcl  17371  glbcl  17384  ismgmid  17650  grpinvf  17853  pj1f  18494  mirf  26011  midf  26124  ismidb  26126  lmif  26133  islmib  26135  uspgredg2vlem  26569  usgredg2vlem1  26571  frgrncvvdeqlem4  27710  grpoidcl  27941  grpoinvcl  27951  pjpreeq  28829  cnlnadjlem3  29500  adjbdln  29514  xdivcld  30193  cvmlift3lem3  31902  nosupno  32438  nosupbday  32440  nosupbnd1  32449  scutcut  32501  transportcl  32729  finxpreclem4  33826  poimirlem26  34063  iorlid  34283  riotaclbgBAD  35110  lshpkrlem2  35267  lshpkrcl  35272  cdleme25cl  36513  cdleme29cl  36533  cdlemefrs29clN  36555  cdlemk29-3  37067  cdlemkid5  37091  dihlsscpre  37390  mapdhcl  37883  hdmapcl  37986  hgmapcl  38045  rernegcl  38181  rersubcl  38189  wessf1ornlem  40298  fourierdlem50  41304