Theorem riotacl 7145

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 3969	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 7144	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sseldi 3875	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃!wreu 3055  {crab 3057  ℩crio 7126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-uni 4797  df-iota 6297  df-riota 7127

This theorem is referenced by:  riotaeqimp  7154  riotaprop  7155  riotass2  7158  riotass  7159  riotaxfrd  7162  riotaclb  7169  supcl  8995  fisupcl  9006  htalem  9398  dfac8clem  9532  dfac2a  9629  fin23lem22  9827  zorn2lem1  9996  subcl  10963  divcl  11382  lbcl  11669  flcl  13256  cjf  14553  sqrtcl  14811  qnumdencl  16179  qnumdenbi  16184  catidcl  17056  lubcl  17711  glbcl  17724  ismgmid  17991  grpinvfval  18260  grpinvf  18268  pj1f  18941  mirf  26606  midf  26722  ismidb  26724  lmif  26731  islmib  26733  uspgredg2vlem  27165  usgredg2vlem1  27167  frgrncvvdeqlem4  28239  grpoidcl  28449  grpoinvcl  28459  pjpreeq  29333  cnlnadjlem3  30004  adjbdln  30018  xdivcld  30772  cvmlift3lem3  32854  nosupno  33549  nosupbday  33551  nosupbnd1  33560  noinfno  33564  noinfbday  33566  noinfbnd1  33575  scutcut  33638  transportcl  33978  finxpreclem4  35208  poimirlem26  35446  iorlid  35659  riotaclbgBAD  36611  lshpkrlem2  36768  lshpkrcl  36773  cdleme25cl  38014  cdleme29cl  38034  cdlemefrs29clN  38056  cdlemk29-3  38568  cdlemkid5  38592  dihlsscpre  38891  mapdhcl  39384  hdmapcl  39487  hgmapcl  39546  fsuppind  39878  rernegcl  39951  rersubcl  39958  sn-subcl  40006  wessf1ornlem  42280  fourierdlem50  43259