Theorem riotacl 7386

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃!wreu 3373  {crab 3431  ℩crio 7367

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6495  df-riota 7368

This theorem is referenced by:  riotaeqimp  7395  riotaprop  7396  riotass2  7399  riotass  7400  riotaxfrd  7403  riotaclb  7410  supcl  9459  fisupcl  9470  ttrcltr  9717  htalem  9897  dfac8clem  10033  dfac2a  10130  fin23lem22  10328  zorn2lem1  10497  subcl  11466  divcl  11885  lbcl  12172  flcl  13767  cjf  15058  sqrtcl  15315  qnumdencl  16682  qnumdenbi  16687  catidcl  17633  lubcl  18320  glbcl  18333  ismgmid  18596  grpinvfval  18906  grpinvf  18914  pj1f  19613  nosupno  27549  nosupbday  27551  nosupbnd1  27560  noinfno  27564  noinfbday  27566  noinfbnd1  27575  scutcut  27647  divsclw  28007  mirf  28344  midf  28460  ismidb  28462  lmif  28469  islmib  28471  uspgredg2vlem  28913  usgredg2vlem1  28915  frgrncvvdeqlem4  29988  grpoidcl  30200  grpoinvcl  30210  pjpreeq  31084  cnlnadjlem3  31755  adjbdln  31769  xdivcld  32522  cvmlift3lem3  34776  transportcl  35475  finxpreclem4  36739  poimirlem26  36978  iorlid  37190  riotaclbgBAD  38288  lshpkrlem2  38445  lshpkrcl  38450  cdleme25cl  39692  cdleme29cl  39712  cdlemefrs29clN  39734  cdlemk29-3  40246  cdlemkid5  40270  dihlsscpre  40569  mapdhcl  41062  hdmapcl  41165  hgmapcl  41224  fsuppind  41625  rernegcl  41707  rersubcl  41714  sn-subcl  41763  tfsconcatfv  42554  wessf1ornlem  44343  fourierdlem50  45331