Theorem riotacl 7320

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃!wreu 3344  {crab 3395  ℩crio 7302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-un 3902  df-ss 3914  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-riota 7303

This theorem is referenced by:  riotaeqimp  7329  riotaprop  7330  riotass2  7333  riotass  7334  riotaxfrd  7337  riotaclb  7344  supcl  9342  fisupcl  9354  ttrcltr  9606  htalem  9789  dfac8clem  9923  dfac2a  10021  fin23lem22  10218  zorn2lem1  10387  subcl  11359  divcl  11782  lbcl  12073  flcl  13699  cjf  15011  sqrtcl  15269  qnumdencl  16650  qnumdenbi  16655  catidcl  17588  lubcl  18261  glbcl  18274  ismgmid  18573  grpinvfval  18891  grpinvf  18899  pj1f  19609  nosupno  27642  nosupbday  27644  nosupbnd1  27653  noinfno  27657  noinfbday  27659  noinfbnd1  27668  scutcut  27742  divsclw  28134  mirf  28638  midf  28754  ismidb  28756  lmif  28763  islmib  28765  uspgredg2vlem  29201  usgredg2vlem1  29203  frgrncvvdeqlem4  30282  grpoidcl  30494  grpoinvcl  30504  pjpreeq  31378  cnlnadjlem3  32049  adjbdln  32063  xdivcld  32903  cvmlift3lem3  35365  transportcl  36077  finxpreclem4  37438  poimirlem26  37696  iorlid  37908  riotaclbgBAD  39063  lshpkrlem2  39220  lshpkrcl  39225  cdleme25cl  40466  cdleme29cl  40486  cdlemefrs29clN  40508  cdlemk29-3  41020  cdlemkid5  41044  dihlsscpre  41343  mapdhcl  41836  hdmapcl  41939  hgmapcl  41998  primrootsunit1  42200  rernegcl  42474  rersubcl  42481  sn-subcl  42531  sn-redivcld  42547  fsuppind  42693  tfsconcatfv  43444  wessf1ornlem  45292  fourierdlem50  46264