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  17623  lubcl  18296  glbcl  18309  ismgmid  18574  grpinvfval  18892  grpinvf  18900  pj1f  19611  nosupno  27648  nosupbday  27650  nosupbnd1  27659  noinfno  27663  noinfbday  27665  noinfbnd1  27674  scutcut  27747  divsclw  28138  mirf  28640  midf  28756  ismidb  28758  lmif  28765  islmib  28767  uspgredg2vlem  29203  usgredg2vlem1  29205  frgrncvvdeqlem4  30281  grpoidcl  30493  grpoinvcl  30503  pjpreeq  31377  cnlnadjlem3  32048  adjbdln  32062  xdivcld  32893  cvmlift3lem3  35301  transportcl  36014  finxpreclem4  37375  poimirlem26  37633  iorlid  37845  riotaclbgBAD  38940  lshpkrlem2  39097  lshpkrcl  39102  cdleme25cl  40344  cdleme29cl  40364  cdlemefrs29clN  40386  cdlemk29-3  40898  cdlemkid5  40922  dihlsscpre  41221  mapdhcl  41714  hdmapcl  41817  hgmapcl  41876  primrootsunit1  42078  rernegcl  42352  rersubcl  42359  sn-subcl  42409  sn-redivcld  42425  fsuppind  42571  tfsconcatfv  43323  wessf1ornlem  45172  fourierdlem50  46147