Theorem riotacl 7361

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃!wreu 3352  {crab 3405  ℩crio 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-riota 7344

This theorem is referenced by:  riotaeqimp  7370  riotaprop  7371  riotass2  7374  riotass  7375  riotaxfrd  7378  riotaclb  7385  supcl  9409  fisupcl  9421  ttrcltr  9669  htalem  9849  dfac8clem  9985  dfac2a  10083  fin23lem22  10280  zorn2lem1  10449  subcl  11420  divcl  11843  lbcl  12134  flcl  13757  cjf  15070  sqrtcl  15328  qnumdencl  16709  qnumdenbi  16714  catidcl  17643  lubcl  18316  glbcl  18329  ismgmid  18592  grpinvfval  18910  grpinvf  18918  pj1f  19627  nosupno  27615  nosupbday  27617  nosupbnd1  27626  noinfno  27630  noinfbday  27632  noinfbnd1  27641  scutcut  27713  divsclw  28098  mirf  28587  midf  28703  ismidb  28705  lmif  28712  islmib  28714  uspgredg2vlem  29150  usgredg2vlem1  29152  frgrncvvdeqlem4  30231  grpoidcl  30443  grpoinvcl  30453  pjpreeq  31327  cnlnadjlem3  31998  adjbdln  32012  xdivcld  32843  cvmlift3lem3  35308  transportcl  36021  finxpreclem4  37382  poimirlem26  37640  iorlid  37852  riotaclbgBAD  38947  lshpkrlem2  39104  lshpkrcl  39109  cdleme25cl  40351  cdleme29cl  40371  cdlemefrs29clN  40393  cdlemk29-3  40905  cdlemkid5  40929  dihlsscpre  41228  mapdhcl  41721  hdmapcl  41824  hgmapcl  41883  primrootsunit1  42085  rernegcl  42359  rersubcl  42366  sn-subcl  42416  sn-redivcld  42432  fsuppind  42578  tfsconcatfv  43330  wessf1ornlem  45179  fourierdlem50  46154