Theorem riotacl 7341

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃!wreu 3340  {crab 3389  ℩crio 7323

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-riota 7324

This theorem is referenced by:  riotaeqimp  7350  riotaprop  7351  riotass2  7354  riotass  7355  riotaxfrd  7358  riotaclb  7365  supcl  9371  fisupcl  9383  ttrcltr  9637  htalem  9820  dfac8clem  9954  dfac2a  10052  fin23lem22  10249  zorn2lem1  10418  subcl  11392  divcl  11815  lbcl  12107  flcl  13754  cjf  15066  sqrtcl  15324  qnumdencl  16709  qnumdenbi  16714  catidcl  17648  lubcl  18321  glbcl  18334  ismgmid  18633  grpinvfval  18954  grpinvf  18962  pj1f  19672  nosupno  27667  nosupbday  27669  nosupbnd1  27678  noinfno  27682  noinfbday  27684  noinfbnd1  27693  cutcuts  27773  divsclw  28187  mirf  28728  midf  28844  ismidb  28846  lmif  28853  islmib  28855  uspgredg2vlem  29292  usgredg2vlem1  29294  frgrncvvdeqlem4  30372  grpoidcl  30585  grpoinvcl  30595  pjpreeq  31469  cnlnadjlem3  32140  adjbdln  32154  xdivcld  32982  cvmlift3lem3  35503  transportcl  36215  finxpreclem4  37710  poimirlem26  37967  iorlid  38179  riotaclbgBAD  39400  lshpkrlem2  39557  lshpkrcl  39562  cdleme25cl  40803  cdleme29cl  40823  cdlemefrs29clN  40845  cdlemk29-3  41357  cdlemkid5  41381  dihlsscpre  41680  mapdhcl  42173  hdmapcl  42276  hgmapcl  42335  primrootsunit1  42536  rernegcl  42803  rersubcl  42810  sn-subcl  42860  sn-redivcld  42876  fsuppind  43023  tfsconcatfv  43769  wessf1ornlem  45615  fourierdlem50  46584