Theorem riotacl 7425

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃!wreu 3367  {crab 3416  ℩crio 7407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4873  df-iota 6520  df-riota 7408

This theorem is used by:  riotaeqimp  7434  riotaprop  7435  riotass2  7438  riotass  7439  riotaxfrd  7442  riotaclb  7449  supcl  9487  fisupcl  9499  ttrcltr  9754  htalem  9998  dfac8clem  10150  dfac2a  10247  fin23lem22  10444  zorn2lem1  10613  subcl  11595  divcl  12020  lbcl  12308  flcl  13975  cjf  15314  sqrtcl  15573  qnumdencl  16959  qnumdenbi  16964  catidcl  17906  lubcl  18579  glbcl  18592  ismgmid  18895  grpinvfval  19239  grpinvf  19247  pj1f  19962  nosupno  28117  nosupbday  28119  nosupbnd1  28128  noinfno  28132  noinfbday  28134  noinfbnd1  28143  cutcuts  28224  divsclw  28638  mirf  29189  midf  29338  ismidb  29340  lmif  29347  islmib  29349  uspgredg2vlem  29861  usgredg2vlem1  29863  frgrncvvdeqlem4  30960  grpoidcl  31173  grpoinvcl  31183  pjpreeq  32057  cnlnadjlem3  32728  adjbdln  32742  xdivcld  33585  cvmlift3lem3  36294  transportcl  37013  finxpreclem4  38585  poimirlem26  38832  iorlid  39058  riotaclbgBAD  40277  lshpkrlem2  40434  lshpkrcl  40439  cdleme25cl  41680  cdleme29cl  41700  cdlemefrs29clN  41722  cdlemk29-3  42234  cdlemkid5  42258  dihlsscpre  42557  mapdhcl  43050  hdmapcl  43153  hgmapcl  43212  primrootsunit1  43413  rernegcl  43688  rersubcl  43695  sn-subcl  43745  sn-redivcld  43761  fsuppind  43884  tfsconcatfv  44604  wessf1ornlem  46473  fourierdlem50  47439