Theorem riotacl 7422

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃!wreu 3386  {crab 3443  ℩crio 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-riota 7404

This theorem is referenced by:  riotaeqimp  7431  riotaprop  7432  riotass2  7435  riotass  7436  riotaxfrd  7439  riotaclb  7446  supcl  9527  fisupcl  9538  ttrcltr  9785  htalem  9965  dfac8clem  10101  dfac2a  10199  fin23lem22  10396  zorn2lem1  10565  subcl  11535  divcl  11955  lbcl  12246  flcl  13846  cjf  15153  sqrtcl  15410  qnumdencl  16786  qnumdenbi  16791  catidcl  17740  lubcl  18427  glbcl  18440  ismgmid  18703  grpinvfval  19018  grpinvf  19026  pj1f  19739  nosupno  27766  nosupbday  27768  nosupbnd1  27777  noinfno  27781  noinfbday  27783  noinfbnd1  27792  scutcut  27864  divsclw  28238  mirf  28686  midf  28802  ismidb  28804  lmif  28811  islmib  28813  uspgredg2vlem  29258  usgredg2vlem1  29260  frgrncvvdeqlem4  30334  grpoidcl  30546  grpoinvcl  30556  pjpreeq  31430  cnlnadjlem3  32101  adjbdln  32115  xdivcld  32887  cvmlift3lem3  35289  transportcl  35997  finxpreclem4  37360  poimirlem26  37606  iorlid  37818  riotaclbgBAD  38910  lshpkrlem2  39067  lshpkrcl  39072  cdleme25cl  40314  cdleme29cl  40334  cdlemefrs29clN  40356  cdlemk29-3  40868  cdlemkid5  40892  dihlsscpre  41191  mapdhcl  41684  hdmapcl  41787  hgmapcl  41846  primrootsunit1  42054  rernegcl  42347  rersubcl  42354  sn-subcl  42403  fsuppind  42545  tfsconcatfv  43303  wessf1ornlem  45092  fourierdlem50  46077