Theorem riotacl 7343

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃!wreu 3349  {crab 3402  ℩crio 7325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  riotaeqimp  7352  riotaprop  7353  riotass2  7356  riotass  7357  riotaxfrd  7360  riotaclb  7367  supcl  9385  fisupcl  9397  ttrcltr  9645  htalem  9825  dfac8clem  9961  dfac2a  10059  fin23lem22  10256  zorn2lem1  10425  subcl  11396  divcl  11819  lbcl  12110  flcl  13733  cjf  15046  sqrtcl  15304  qnumdencl  16685  qnumdenbi  16690  catidcl  17619  lubcl  18292  glbcl  18305  ismgmid  18568  grpinvfval  18886  grpinvf  18894  pj1f  19603  nosupno  27591  nosupbday  27593  nosupbnd1  27602  noinfno  27606  noinfbday  27608  noinfbnd1  27617  scutcut  27689  divsclw  28074  mirf  28563  midf  28679  ismidb  28681  lmif  28688  islmib  28690  uspgredg2vlem  29126  usgredg2vlem1  29128  frgrncvvdeqlem4  30204  grpoidcl  30416  grpoinvcl  30426  pjpreeq  31300  cnlnadjlem3  31971  adjbdln  31985  xdivcld  32816  cvmlift3lem3  35281  transportcl  35994  finxpreclem4  37355  poimirlem26  37613  iorlid  37825  riotaclbgBAD  38920  lshpkrlem2  39077  lshpkrcl  39082  cdleme25cl  40324  cdleme29cl  40344  cdlemefrs29clN  40366  cdlemk29-3  40878  cdlemkid5  40902  dihlsscpre  41201  mapdhcl  41694  hdmapcl  41797  hgmapcl  41856  primrootsunit1  42058  rernegcl  42332  rersubcl  42339  sn-subcl  42389  sn-redivcld  42405  fsuppind  42551  tfsconcatfv  43303  wessf1ornlem  45152  fourierdlem50  46127