Theorem riotacl 7330

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃!wreu 3342  {crab 3391  ℩crio 7312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-un 3888  df-ss 3900  df-sn 4556  df-pr 4558  df-uni 4839  df-iota 6441  df-riota 7313

This theorem is referenced by:  riotaeqimp  7339  riotaprop  7340  riotass2  7343  riotass  7344  riotaxfrd  7347  riotaclb  7354  supcl  9361  fisupcl  9373  ttrcltr  9628  htalem  9811  dfac8clem  9945  dfac2a  10043  fin23lem22  10240  zorn2lem1  10409  subcl  11383  divcl  11806  lbcl  12098  flcl  13745  cjf  15057  sqrtcl  15315  qnumdencl  16700  qnumdenbi  16705  catidcl  17639  lubcl  18312  glbcl  18325  ismgmid  18624  grpinvfval  18945  grpinvf  18953  pj1f  19663  nosupno  27685  nosupbday  27687  nosupbnd1  27696  noinfno  27700  noinfbday  27702  noinfbnd1  27711  cutcuts  27791  divsclw  28205  mirf  28746  midf  28862  ismidb  28864  lmif  28871  islmib  28873  uspgredg2vlem  29310  usgredg2vlem1  29312  frgrncvvdeqlem4  30390  grpoidcl  30603  grpoinvcl  30613  pjpreeq  31487  cnlnadjlem3  32158  adjbdln  32172  xdivcld  33001  cvmlift3lem3  35549  transportcl  36261  finxpreclem4  37756  poimirlem26  38013  iorlid  38225  riotaclbgBAD  39446  lshpkrlem2  39603  lshpkrcl  39608  cdleme25cl  40849  cdleme29cl  40869  cdlemefrs29clN  40891  cdlemk29-3  41403  cdlemkid5  41427  dihlsscpre  41726  mapdhcl  42219  hdmapcl  42322  hgmapcl  42381  primrootsunit1  42582  rernegcl  42848  rersubcl  42855  sn-subcl  42905  sn-redivcld  42921  fsuppind  43040  tfsconcatfv  43786  wessf1ornlem  45632  fourierdlem50  46599