Theorem riotacl 7394

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃!wreu 3364  {crab 3413  ℩crio 7376

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6494  df-riota 7377

This theorem is used by:  riotaeqimp  7403  riotaprop  7404  riotass2  7407  riotass  7408  riotaxfrd  7411  riotaclb  7418  supcl  9450  fisupcl  9462  ttrcltr  9717  htalem  9961  dfac8clem  10111  dfac2a  10208  fin23lem22  10405  zorn2lem1  10574  subcl  11556  divcl  11980  lbcl  12268  flcl  13935  cjf  15271  sqrtcl  15529  qnumdencl  16915  qnumdenbi  16920  catidcl  17856  lubcl  18529  glbcl  18542  ismgmid  18845  grpinvfval  19189  grpinvf  19197  pj1f  19911  nosupno  28060  nosupbday  28062  nosupbnd1  28071  noinfno  28075  noinfbday  28077  noinfbnd1  28086  cutcuts  28167  divsclw  28581  mirf  29132  midf  29281  ismidb  29283  lmif  29290  islmib  29292  uspgredg2vlem  29804  usgredg2vlem1  29806  frgrncvvdeqlem4  30903  grpoidcl  31116  grpoinvcl  31126  pjpreeq  32000  cnlnadjlem3  32671  adjbdln  32685  xdivcld  33489  cvmlift3lem3  36086  transportcl  36798  finxpreclem4  38317  poimirlem26  38564  iorlid  38792  riotaclbgBAD  40011  lshpkrlem2  40168  lshpkrcl  40173  cdleme25cl  41414  cdleme29cl  41434  cdlemefrs29clN  41456  cdlemk29-3  41968  cdlemkid5  41992  dihlsscpre  42291  mapdhcl  42784  hdmapcl  42887  hgmapcl  42946  primrootsunit1  43147  rernegcl  43422  rersubcl  43429  sn-subcl  43479  sn-redivcld  43495  fsuppind  43618  tfsconcatfv  44342  wessf1ornlem  46199  fourierdlem50  47165