Theorem riotacl 7388

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃!wreu 3363  {crab 3412  ℩crio 7370

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 2732

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6489  df-riota 7371

This theorem is used by:  riotaeqimp  7397  riotaprop  7398  riotass2  7401  riotass  7402  riotaxfrd  7405  riotaclb  7412  supcl  9429  fisupcl  9441  ttrcltr  9696  htalem  9901  dfac8clem  10036  dfac2a  10133  fin23lem22  10330  zorn2lem1  10499  subcl  11481  divcl  11903  lbcl  12191  flcl  13857  cjf  15192  sqrtcl  15450  qnumdencl  16831  qnumdenbi  16836  catidcl  17771  lubcl  18444  glbcl  18457  ismgmid  18759  grpinvfval  19103  grpinvf  19111  pj1f  19825  nosupno  27940  nosupbday  27942  nosupbnd1  27951  noinfno  27955  noinfbday  27957  noinfbnd1  27966  cutcuts  28047  divsclw  28461  mirf  29012  midf  29161  ismidb  29163  lmif  29170  islmib  29172  uspgredg2vlem  29684  usgredg2vlem1  29686  frgrncvvdeqlem4  30783  grpoidcl  30996  grpoinvcl  31006  pjpreeq  31880  cnlnadjlem3  32551  adjbdln  32565  xdivcld  33369  cvmlift3lem3  35901  transportcl  36614  finxpreclem4  38149  poimirlem26  38396  iorlid  38609  riotaclbgBAD  39828  lshpkrlem2  39985  lshpkrcl  39990  cdleme25cl  41231  cdleme29cl  41251  cdlemefrs29clN  41273  cdlemk29-3  41785  cdlemkid5  41809  dihlsscpre  42108  mapdhcl  42601  hdmapcl  42704  hgmapcl  42763  primrootsunit1  42964  rernegcl  43247  rersubcl  43254  sn-subcl  43304  sn-redivcld  43320  fsuppind  43437  tfsconcatfv  44183  wessf1ornlem  46018  fourierdlem50  46985