Theorem riotacl 7335

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃!wreu 3341  {crab 3390  ℩crio 7317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6449  df-riota 7318

This theorem is referenced by:  riotaeqimp  7344  riotaprop  7345  riotass2  7348  riotass  7349  riotaxfrd  7352  riotaclb  7359  supcl  9365  fisupcl  9377  ttrcltr  9631  htalem  9814  dfac8clem  9948  dfac2a  10046  fin23lem22  10243  zorn2lem1  10412  subcl  11386  divcl  11809  lbcl  12101  flcl  13748  cjf  15060  sqrtcl  15318  qnumdencl  16703  qnumdenbi  16708  catidcl  17642  lubcl  18315  glbcl  18328  ismgmid  18627  grpinvfval  18948  grpinvf  18956  pj1f  19666  nosupno  27684  nosupbday  27686  nosupbnd1  27695  noinfno  27699  noinfbday  27701  noinfbnd1  27710  cutcuts  27790  divsclw  28204  mirf  28745  midf  28861  ismidb  28863  lmif  28870  islmib  28872  uspgredg2vlem  29309  usgredg2vlem1  29311  frgrncvvdeqlem4  30390  grpoidcl  30603  grpoinvcl  30613  pjpreeq  31487  cnlnadjlem3  32158  adjbdln  32172  xdivcld  33000  cvmlift3lem3  35522  transportcl  36234  finxpreclem4  37727  poimirlem26  37984  iorlid  38196  riotaclbgBAD  39417  lshpkrlem2  39574  lshpkrcl  39579  cdleme25cl  40820  cdleme29cl  40840  cdlemefrs29clN  40862  cdlemk29-3  41374  cdlemkid5  41398  dihlsscpre  41697  mapdhcl  42190  hdmapcl  42293  hgmapcl  42352  primrootsunit1  42553  rernegcl  42820  rersubcl  42827  sn-subcl  42877  sn-redivcld  42893  fsuppind  43040  tfsconcatfv  43790  wessf1ornlem  45636  fourierdlem50  46605