Theorem riotacl 7250

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃!wreu 3066  {crab 3068  ℩crio 7231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564  df-uni 4840  df-iota 6391  df-riota 7232

This theorem is referenced by:  riotaeqimp  7259  riotaprop  7260  riotass2  7263  riotass  7264  riotaxfrd  7267  riotaclb  7274  supcl  9217  fisupcl  9228  ttrcltr  9474  htalem  9654  dfac8clem  9788  dfac2a  9885  fin23lem22  10083  zorn2lem1  10252  subcl  11220  divcl  11639  lbcl  11926  flcl  13515  cjf  14815  sqrtcl  15073  qnumdencl  16443  qnumdenbi  16448  catidcl  17391  lubcl  18075  glbcl  18088  ismgmid  18349  grpinvfval  18618  grpinvf  18626  pj1f  19303  mirf  27021  midf  27137  ismidb  27139  lmif  27146  islmib  27148  uspgredg2vlem  27590  usgredg2vlem1  27592  frgrncvvdeqlem4  28666  grpoidcl  28876  grpoinvcl  28886  pjpreeq  29760  cnlnadjlem3  30431  adjbdln  30445  xdivcld  31197  cvmlift3lem3  33283  nosupno  33906  nosupbday  33908  nosupbnd1  33917  noinfno  33921  noinfbday  33923  noinfbnd1  33932  scutcut  33995  transportcl  34335  finxpreclem4  35565  poimirlem26  35803  iorlid  36016  riotaclbgBAD  36968  lshpkrlem2  37125  lshpkrcl  37130  cdleme25cl  38371  cdleme29cl  38391  cdlemefrs29clN  38413  cdlemk29-3  38925  cdlemkid5  38949  dihlsscpre  39248  mapdhcl  39741  hdmapcl  39844  hgmapcl  39903  fsuppind  40279  rernegcl  40354  rersubcl  40361  sn-subcl  40409  wessf1ornlem  42722  fourierdlem50  43697