Theorem riotacl 7323

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃!wreu 3341  {crab 3394  ℩crio 7305

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-un 3908  df-ss 3920  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-riota 7306

This theorem is referenced by:  riotaeqimp  7332  riotaprop  7333  riotass2  7336  riotass  7337  riotaxfrd  7340  riotaclb  7347  supcl  9348  fisupcl  9360  ttrcltr  9612  htalem  9792  dfac8clem  9926  dfac2a  10024  fin23lem22  10221  zorn2lem1  10390  subcl  11362  divcl  11785  lbcl  12076  flcl  13699  cjf  15011  sqrtcl  15269  qnumdencl  16650  qnumdenbi  16655  catidcl  17588  lubcl  18261  glbcl  18274  ismgmid  18539  grpinvfval  18857  grpinvf  18865  pj1f  19576  nosupno  27613  nosupbday  27615  nosupbnd1  27624  noinfno  27628  noinfbday  27630  noinfbnd1  27639  scutcut  27712  divsclw  28103  mirf  28605  midf  28721  ismidb  28723  lmif  28730  islmib  28732  uspgredg2vlem  29168  usgredg2vlem1  29170  frgrncvvdeqlem4  30246  grpoidcl  30458  grpoinvcl  30468  pjpreeq  31342  cnlnadjlem3  32013  adjbdln  32027  xdivcld  32863  cvmlift3lem3  35298  transportcl  36011  finxpreclem4  37372  poimirlem26  37630  iorlid  37842  riotaclbgBAD  38937  lshpkrlem2  39094  lshpkrcl  39099  cdleme25cl  40340  cdleme29cl  40360  cdlemefrs29clN  40382  cdlemk29-3  40894  cdlemkid5  40918  dihlsscpre  41217  mapdhcl  41710  hdmapcl  41813  hgmapcl  41872  primrootsunit1  42074  rernegcl  42348  rersubcl  42355  sn-subcl  42405  sn-redivcld  42421  fsuppind  42567  tfsconcatfv  43318  wessf1ornlem  45167  fourierdlem50  46141